more direct access to atomic cterms;

--- a/src/HOL/Decision_Procs/ferrante_rackoff.ML	Tue Jul 28 18:59:15 2015 +0200
+++ b/src/HOL/Decision_Procs/ferrante_rackoff.ML	Tue Jul 28 19:49:54 2015 +0200
@@ -206,7 +206,7 @@
    val pcv = Simplifier.rewrite (put_simpset ss' ctxt);
    val postcv = Simplifier.rewrite (put_simpset ss ctxt);
    val nnf = K (nnf_conv ctxt then_conv postcv)
-   val qe_conv = Qelim.gen_qelim_conv pcv postcv pcv cons (Thm.add_cterm_frees tm [])
+   val qe_conv = Qelim.gen_qelim_conv pcv postcv pcv cons (Drule.cterm_add_frees tm [])
                   (isolate_conv ctxt) nnf
                   (fn vs => ferrack_conv ctxt (thy,{isolate_conv = isolate_conv ctxt,
                                                whatis = whatis, simpset = ss}) vs

--- a/src/HOL/Decision_Procs/langford.ML	Tue Jul 28 18:59:15 2015 +0200
+++ b/src/HOL/Decision_Procs/langford.ML	Tue Jul 28 19:49:54 2015 +0200
@@ -191,7 +191,7 @@
   in
     fn p =>
       Qelim.gen_qelim_conv pcv pcv dnfex_conv cons
-        (Thm.add_cterm_frees p []) (K Thm.reflexive) (K Thm.reflexive)
+        (Drule.cterm_add_frees p []) (K Thm.reflexive) (K Thm.reflexive)
         (K (basic_dloqe ctxt gst qe_bnds qe_nolb qe_noub gs)) p
   end;
 

--- a/src/HOL/Library/Sum_of_Squares/sum_of_squares.ML	Tue Jul 28 18:59:15 2015 +0200
+++ b/src/HOL/Library/Sum_of_Squares/sum_of_squares.ML	Tue Jul 28 19:49:54 2015 +0200
@@ -900,9 +900,9 @@
         then (RealArith.dest_ratconst (Thm.dest_arg1 tm), Thm.dest_arg tm)
         else raise Failure "substitutable_monomial"
     | @{term "op + :: real => _"}$_$_ =>
-         (substitutable_monomial (Thm.add_cterm_frees (Thm.dest_arg tm) fvs) (Thm.dest_arg1 tm)
+         (substitutable_monomial (Drule.cterm_add_frees (Thm.dest_arg tm) fvs) (Thm.dest_arg1 tm)
            handle Failure _ =>
-            substitutable_monomial (Thm.add_cterm_frees (Thm.dest_arg1 tm) fvs) (Thm.dest_arg tm))
+            substitutable_monomial (Drule.cterm_add_frees (Thm.dest_arg1 tm) fvs) (Thm.dest_arg tm))
     | _ => raise Failure "substitutable_monomial")
 
   fun isolate_variable v th =

--- a/src/HOL/Tools/Qelim/qelim.ML	Tue Jul 28 18:59:15 2015 +0200
+++ b/src/HOL/Tools/Qelim/qelim.ML	Tue Jul 28 19:49:54 2015 +0200
@@ -65,7 +65,7 @@
 
 fun standard_qelim_conv ctxt atcv ncv qcv p =
   let val pcv = pcv ctxt
-  in gen_qelim_conv pcv pcv pcv cons (Thm.add_cterm_frees p []) atcv ncv qcv p end
+  in gen_qelim_conv pcv pcv pcv cons (Drule.cterm_add_frees p []) atcv ncv qcv p end
 
 end;
 

--- a/src/HOL/Tools/groebner.ML	Tue Jul 28 18:59:15 2015 +0200
+++ b/src/HOL/Tools/groebner.ML	Tue Jul 28 19:49:54 2015 +0200
@@ -532,7 +532,7 @@
  fun simp_ex_conv ctxt =
    Simplifier.rewrite (put_simpset HOL_basic_ss ctxt addsimps @{thms simp_thms(39)})
 
-fun frees t = Thm.add_cterm_frees t [];
+fun frees t = Drule.cterm_add_frees t [];
 fun free_in v t = member op aconvc (frees t) v;
 
 val vsubst = let
@@ -741,7 +741,7 @@
     Thm.apply
       (Drule.cterm_rule (Thm.instantiate' [SOME (Thm.ctyp_of_cterm x)] [])
         @{cpat "All:: (?'a => bool) => _"}) (Thm.lambda x p)
-  val avs = Thm.add_cterm_frees tm []
+  val avs = Drule.cterm_add_frees tm []
   val P' = fold mk_forall avs tm
   val th1 = initial_conv ctxt (mk_neg P')
   val (evs,bod) = strip_exists(concl th1) in
@@ -797,7 +797,7 @@
    val mons = striplist(dest_binary ring_add_tm) t
   in member (op aconvc) mons v andalso
     forall (fn m => v aconvc m
-          orelse not(member (op aconvc) (Thm.add_cterm_frees m []) v)) mons
+          orelse not(member (op aconvc) (Drule.cterm_add_frees m []) v)) mons
   end
 
   fun isolate_variable vars tm =

--- a/src/Pure/drule.ML	Tue Jul 28 18:59:15 2015 +0200
+++ b/src/Pure/drule.ML	Tue Jul 28 19:49:54 2015 +0200
@@ -91,6 +91,8 @@
   val mk_term: cterm -> thm
   val dest_term: thm -> cterm
   val cterm_rule: (thm -> thm) -> cterm -> cterm
+  val cterm_add_frees: cterm -> cterm list -> cterm list
+  val cterm_add_vars: cterm -> cterm list -> cterm list
   val dummy_thm: thm
   val is_sort_constraint: term -> bool
   val sort_constraintI: thm
@@ -174,9 +176,7 @@
 val forall_intr_list = fold_rev Thm.forall_intr;
 
 (*Generalization over Vars -- canonical order*)
-fun forall_intr_vars th =
-  fold Thm.forall_intr
-    (map (Thm.global_cterm_of (Thm.theory_of_thm th) o Var) (Thm.fold_terms Term.add_vars th [])) th;
+fun forall_intr_vars th = fold Thm.forall_intr (Thm.add_vars th []) th;
 
 fun outer_params t =
   let val vs = Term.strip_all_vars t
@@ -631,6 +631,9 @@
 
 fun cterm_rule f = dest_term o f o mk_term;
 
+val cterm_add_frees = Thm.add_frees o mk_term;
+val cterm_add_vars = Thm.add_vars o mk_term;
+
 val dummy_thm = mk_term (certify Term.dummy_prop);
 
 

--- a/src/Pure/more_thm.ML	Tue Jul 28 18:59:15 2015 +0200
+++ b/src/Pure/more_thm.ML	Tue Jul 28 19:49:54 2015 +0200
@@ -21,7 +21,8 @@
   structure Ctermtab: TABLE
   structure Thmtab: TABLE
   val aconvc: cterm * cterm -> bool
-  val add_cterm_frees: cterm -> cterm list -> cterm list
+  val add_frees: thm -> cterm list -> cterm list
+  val add_vars: thm -> cterm list -> cterm list
   val all_name: string * cterm -> cterm -> cterm
   val all: cterm -> cterm -> cterm
   val mk_binop: cterm -> cterm -> cterm -> cterm
@@ -112,13 +113,8 @@
 
 val op aconvc = op aconv o apply2 Thm.term_of;
 
-fun add_cterm_frees ct =
-  let
-    val thy = Thm.theory_of_cterm ct;
-    val t = Thm.term_of ct;
-  in
-    Term.fold_aterms (fn v as Free _ => insert (op aconvc) (Thm.global_cterm_of thy v) | _ => I) t
-  end;
+val add_frees = Thm.fold_atomic_cterms (fn a => is_Free (Thm.term_of a) ? insert (op aconvc) a);
+val add_vars = Thm.fold_atomic_cterms (fn a => is_Var (Thm.term_of a) ? insert (op aconvc) a);
 
 
 (* cterm constructors and destructors *)

--- a/src/Pure/thm.ML	Tue Jul 28 18:59:15 2015 +0200
+++ b/src/Pure/thm.ML	Tue Jul 28 19:49:54 2015 +0200
@@ -69,6 +69,7 @@
     tpairs: (cterm * cterm) list,
     prop: cterm}
   val fold_terms: (term -> 'a -> 'a) -> thm -> 'a -> 'a
+  val fold_atomic_cterms: (cterm -> 'a -> 'a) -> thm -> 'a -> 'a
   val terms_of_tpairs: (term * term) list -> term list
   val full_prop_of: thm -> term
   val theory_of_thm: thm -> theory
@@ -366,6 +367,15 @@
 fun fold_terms f (Thm (_, {tpairs, prop, hyps, ...})) =
   fold (fn (t, u) => f t #> f u) tpairs #> f prop #> fold f hyps;
 
+fun fold_atomic_cterms f (th as Thm (_, {thy, maxidx, shyps, ...})) =
+  let fun cterm t T = Cterm {thy = thy, t = t, T = T, maxidx = maxidx, sorts = shyps} in
+    (fold_terms o fold_aterms)
+      (fn t as Const (_, T) => f (cterm t T)
+        | t as Free (_, T) => f (cterm t T)
+        | t as Var (_, T) => f (cterm t T)
+        | _ => I) th
+  end;
+
 fun terms_of_tpairs tpairs = fold_rev (fn (t, u) => cons t o cons u) tpairs [];
 
 fun eq_tpairs ((t, u), (t', u')) = t aconv t' andalso u aconv u';