# HG changeset patch
# User wenzelm
# Date 1230745996 -3600
# Node ID 1d685baea08efea06a2966aa79c4a6abd5df07ed
# Parent  0eade173f77e702be9376fbf1a81acf188c9dd21
moved old add_type_XXX, add_term_XXX etc. to structure OldTerm;
use exists_Const directly;

diff -r 0eade173f77e -r 1d685baea08e src/HOL/Tools/inductive_realizer.ML
--- a/src/HOL/Tools/inductive_realizer.ML	Wed Dec 31 18:53:16 2008 +0100
+++ b/src/HOL/Tools/inductive_realizer.ML	Wed Dec 31 18:53:16 2008 +0100
@@ -49,7 +49,7 @@
       t $ strip_all' used names Q
   | strip_all' _ _ t = t;
 
-fun strip_all t = strip_all' (add_term_free_names (t, [])) [] t;
+fun strip_all t = strip_all' (OldTerm.add_term_free_names (t, [])) [] t;
 
 fun strip_one name (Const ("all", _) $ Abs (s, T, Const ("==>", _) $ P $ Q)) =
       (subst_bound (Free (name, T), P), subst_bound (Free (name, T), Q))
@@ -63,7 +63,7 @@
 
 fun dt_of_intrs thy vs nparms intrs =
   let
-    val iTs = term_tvars (prop_of (hd intrs));
+    val iTs = OldTerm.term_tvars (prop_of (hd intrs));
     val Tvs = map TVar iTs;
     val (Const (s, _), ts) = strip_comb (HOLogic.dest_Trueprop
       (Logic.strip_imp_concl (prop_of (hd intrs))));
@@ -100,7 +100,7 @@
 fun mk_realizes_eqn n vs nparms intrs =
   let
     val concl = HOLogic.dest_Trueprop (concl_of (hd intrs));
-    val iTs = term_tvars concl;
+    val iTs = OldTerm.term_tvars concl;
     val Tvs = map TVar iTs;
     val (h as Const (s, T), us) = strip_comb concl;
     val params = List.take (us, nparms);
@@ -146,7 +146,7 @@
     val conclT = Extraction.etype_of thy vs [] (Logic.strip_imp_concl rule');
     val used = map (fst o dest_Free) args;
 
-    fun is_rec t = not (null (term_consts t inter rsets));
+    val is_rec = exists_Const (fn (c, _) => member (op =) rsets c);
 
     fun is_meta (Const ("all", _) $ Abs (s, _, P)) = is_meta P
       | is_meta (Const ("==>", _) $ _ $ Q) = is_meta Q
@@ -275,7 +275,7 @@
   let
     val qualifier = NameSpace.qualifier (name_of_thm induct);
     val inducts = PureThy.get_thms thy (NameSpace.qualified qualifier "inducts");
-    val iTs = term_tvars (prop_of (hd intrs));
+    val iTs = OldTerm.term_tvars (prop_of (hd intrs));
     val ar = length vs + length iTs;
     val params = InductivePackage.params_of raw_induct;
     val arities = InductivePackage.arities_of raw_induct;
@@ -370,7 +370,7 @@
           (vs' @ Ps) rec_names rss' intrs dummies;
         val rlzs = map (fn (r, ind) => Extraction.realizes_of thy (vs' @ Ps) r
           (prop_of ind)) (rs ~~ inducts);
-        val used = foldr add_term_free_names [] rlzs;
+        val used = foldr OldTerm.add_term_free_names [] rlzs;
         val rnames = Name.variant_list used (replicate (length inducts) "r");
         val rnames' = Name.variant_list
           (used @ rnames) (replicate (length intrs) "s");
diff -r 0eade173f77e -r 1d685baea08e src/Pure/Proof/proof_rewrite_rules.ML
--- a/src/Pure/Proof/proof_rewrite_rules.ML	Wed Dec 31 18:53:16 2008 +0100
+++ b/src/Pure/Proof/proof_rewrite_rules.ML	Wed Dec 31 18:53:16 2008 +0100
@@ -1,5 +1,4 @@
 (*  Title:      Pure/Proof/proof_rewrite_rules.ML
-    ID:         $Id$
     Author:     Stefan Berghofer, TU Muenchen
 
 Simplification functions for proof terms involving meta level rules.
@@ -196,7 +195,8 @@
   let
     fun rew_term Ts t =
       let
-        val frees = map Free (Name.invent_list (add_term_names (t, [])) "xa" (length Ts) ~~ Ts);
+        val frees =
+          map Free (Name.invent_list (OldTerm.add_term_names (t, [])) "xa" (length Ts) ~~ Ts);
         val t' = r (subst_bounds (frees, t));
         fun strip [] t = t
           | strip (_ :: xs) (Abs (_, _, t)) = strip xs t;
@@ -228,7 +228,7 @@
           if member (op =) defs s then
             let
               val vs = vars_of prop;
-              val tvars = term_tvars prop;
+              val tvars = OldTerm.term_tvars prop;
               val (_, rhs) = Logic.dest_equals prop;
               val rhs' = Term.betapplys (subst_TVars (map fst tvars ~~ Ts)
                 (fold_rev (fn x => fn b => Abs ("", dummyT, abstract_over (x, b))) vs rhs),
@@ -249,7 +249,9 @@
         val cnames = map (fst o dest_Const o fst) defs';
         val thms = fold_proof_atoms true
           (fn PThm (_, ((name, prop, _), _)) =>
-              if member (op =) defnames name orelse null (term_consts prop inter cnames) then I
+              if member (op =) defnames name orelse
+                not (exists_Const (member (op =) cnames o #1) prop)
+              then I
               else cons (name, SOME prop)
             | _ => I) [prf] [];
       in Reconstruct.expand_proof thy thms end;