# HG changeset patch # User wenzelm # Date 1438107319 -7200 # Node ID f7f4d5f7920e20f8adcbd1d7948b8de7dfa4ac5b # Parent d0a88a2182a80b972228ec1d98953fb522b7119b more direct access to atomic cterms; diff -r d0a88a2182a8 -r f7f4d5f7920e src/Pure/more_thm.ML --- a/src/Pure/more_thm.ML Tue Jul 28 20:07:05 2015 +0200 +++ b/src/Pure/more_thm.ML Tue Jul 28 20:15:19 2015 +0200 @@ -367,9 +367,12 @@ val thy = Thm.theory_of_thm th; val {prop, hyps, tpairs, ...} = Thm.rep_thm th; val fixed = fold Term.add_frees (Thm.terms_of_tpairs tpairs @ hyps) []; - val frees = Term.fold_aterms (fn Free v => - if member (op =) fixed v then I else insert (op =) v | _ => I) prop []; - in fold (Thm.forall_intr o Thm.global_cterm_of thy o Free) frees th end; + val frees = + Thm.fold_atomic_cterms (fn a => + (case Thm.term_of a of + Free v => not (member (op =) fixed v) ? insert (op aconvc) a + | _ => I)) th []; + in fold Thm.forall_intr frees th end; (* unvarify_global: global schematic variables *)