Skip to content

Commit f3101b2

Browse files
committed
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 24e40cd commit f3101b2

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
@@ -782,7 +782,7 @@ in
782782
if is_forall (concl th) then
783783
let
784784
val (hvs, con) = (HOLset.listItems ## I) (hyp_frees th, concl th)
785-
val fvs = free_vars con
785+
val fvs = HOLset.listItems (FVL [con] empty_tmset)
786786
val vars = fst (strip_forall con)
787787
in
788788
SPECL (snd (itlist varyAcc vars (hvs @ fvs, []))) th

0 commit comments

Comments
 (0)