# 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 *)