Skip to content

Commit 03ff3ca

Browse files
ordinarymathmn200
authored andcommitted
Speed up SPEC_ALL
Note that reusing set from hyp_frees is actually slower. times using `time bin/build` before real 10m37.510s user 21m43.869s sys 3m12.949s reusing set from hyp_frees real 10m40.847s user 21m49.628s sys 3m16.913s without reusing set from hyp_frees real 10m29.285s user 21m9.849s sys 3m10.606s
1 parent 1caa504 commit 03ff3ca

File tree

1 file changed

+1
-1
lines changed

1 file changed

+1
-1
lines changed

src/1/Drule.sml

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -803,7 +803,7 @@ in
803803
if is_forall (concl th) then
804804
let
805805
val (hvs, con) = (HOLset.listItems ## I) (hyp_frees th, concl th)
806-
val fvs = free_vars con
806+
val fvs = HOLset.listItems (FVL [con] empty_tmset)
807807
val vars = fst (strip_forall con)
808808
in
809809
SPECL (snd (itlist varyAcc vars (hvs @ fvs, []))) th

0 commit comments

Comments
 (0)