# HG changeset patch
# User wenzelm
# Date 1176640307 -7200
# Node ID 290454649b8cdcd6201fd892786f84f35710bb6a
# Parent  0b08f218f260fd724cd3582c86b0035775844a47
Thm.fold_terms;

diff -r 0b08f218f260 -r 290454649b8c src/HOL/Import/proof_kernel.ML
--- a/src/HOL/Import/proof_kernel.ML	Sun Apr 15 14:31:44 2007 +0200
+++ b/src/HOL/Import/proof_kernel.ML	Sun Apr 15 14:31:47 2007 +0200
@@ -2199,9 +2199,9 @@
 		    [NONE, NONE, NONE, SOME (cterm_of thy' (Free ("a", aty))), SOME (cterm_of thy' (Free ("r", tT)))]
                     typedef_hol2hollight
 	    val th4 = (#type_definition typedef_info) RS typedef_hol2hollight'
-            val _ = null (Drule.fold_terms Term.add_tvars th4 []) orelse
+            val _ = null (Thm.fold_terms Term.add_tvars th4 []) orelse
               raise ERR "type_introduction" "no type variables expected any more"
-            val _ = null (Drule.fold_terms Term.add_vars th4 []) orelse
+            val _ = null (Thm.fold_terms Term.add_vars th4 []) orelse
               raise ERR "type_introduction" "no term variables expected any more"
 	    val _ = message ("step 3: thyname="^thyname^", tycname="^tycname^", fulltyname="^fulltyname)
             val thy'' = add_hol4_type_mapping thyname tycname true fulltyname thy'
diff -r 0b08f218f260 -r 290454649b8c src/HOL/Tools/datatype_realizer.ML
--- a/src/HOL/Tools/datatype_realizer.ML	Sun Apr 15 14:31:44 2007 +0200
+++ b/src/HOL/Tools/datatype_realizer.ML	Sun Apr 15 14:31:47 2007 +0200
@@ -136,7 +136,7 @@
       ||> Theory.restore_naming thy;
 
     val ivs = rev (Term.add_vars (Logic.varify (DatatypeProp.make_ind [descr] sorts)) []);
-    val rvs = rev (Drule.fold_terms Term.add_vars thm' []);
+    val rvs = rev (Thm.fold_terms Term.add_vars thm' []);
     val ivs1 = map Var (filter_out (fn (_, T) =>
       tname_of (body_type T) mem ["set", "bool"]) ivs);
     val ivs2 = map (fn (ixn, _) => Var (ixn, valOf (AList.lookup (op =) rvs ixn))) ivs;
diff -r 0b08f218f260 -r 290454649b8c src/HOL/Tools/res_axioms.ML
--- a/src/HOL/Tools/res_axioms.ML	Sun Apr 15 14:31:44 2007 +0200
+++ b/src/HOL/Tools/res_axioms.ML	Sun Apr 15 14:31:47 2007 +0200
@@ -152,7 +152,7 @@
 
 (*Returns the vars of a theorem*)
 fun vars_of_thm th =
-  map (Thm.cterm_of (theory_of_thm th) o Var) (Drule.fold_terms Term.add_vars th []);
+  map (Thm.cterm_of (theory_of_thm th) o Var) (Thm.fold_terms Term.add_vars th []);
 
 (*Make a version of fun_cong with a given variable name*)
 local
diff -r 0b08f218f260 -r 290454649b8c src/Pure/Isar/element.ML
--- a/src/Pure/Isar/element.ML	Sun Apr 15 14:31:44 2007 +0200
+++ b/src/Pure/Isar/element.ML	Sun Apr 15 14:31:47 2007 +0200
@@ -374,7 +374,7 @@
 fun rename_thm ren th =
   let
     val thy = Thm.theory_of_thm th;
-    val subst = (Drule.fold_terms o Term.fold_aterms)
+    val subst = (Thm.fold_terms o Term.fold_aterms)
       (fn Free (x, T) =>
         let val x' = rename ren x
         in if x = x' then I else insert (eq_fst (op =)) ((x, T), Free (x', T)) end
@@ -398,7 +398,7 @@
   if Symtab.is_empty env then I
   else Term.map_types (instT_type env);
 
-fun instT_subst env th = (Drule.fold_terms o Term.fold_types o Term.fold_atyps)
+fun instT_subst env th = (Thm.fold_terms o Term.fold_types o Term.fold_atyps)
   (fn T as TFree (a, _) =>
     let val T' = the_default T (Symtab.lookup env a)
     in if T = T' then I else insert (op =) (a, T') end
@@ -443,7 +443,7 @@
   else
     let
       val substT = instT_subst envT th;
-      val subst = (Drule.fold_terms o Term.fold_aterms)
+      val subst = (Thm.fold_terms o Term.fold_aterms)
        (fn Free (x, T) =>
           let
             val T' = instT_type envT T;
diff -r 0b08f218f260 -r 290454649b8c src/Pure/Isar/local_defs.ML
--- a/src/Pure/Isar/local_defs.ML	Sun Apr 15 14:31:44 2007 +0200
+++ b/src/Pure/Isar/local_defs.ML	Sun Apr 15 14:31:47 2007 +0200
@@ -109,7 +109,7 @@
   in fn th =>
     let
       val th' = exp th;
-      val still_fixed = map #1 (Drule.fold_terms Term.add_frees th' []);
+      val still_fixed = map #1 (Thm.fold_terms Term.add_frees th' []);
       val defs = prems |> filter_out (fn prem =>
         (case try (head_of_def o Thm.prop_of) prem of
           SOME x => member (op =) still_fixed x
diff -r 0b08f218f260 -r 290454649b8c src/Pure/axclass.ML
--- a/src/Pure/axclass.ML	Sun Apr 15 14:31:44 2007 +0200
+++ b/src/Pure/axclass.ML	Sun Apr 15 14:31:47 2007 +0200
@@ -214,7 +214,7 @@
 fun add_classrel th thy =
   let
     fun err () = raise THM ("add_classrel: malformed class relation", 0, [th]);
-    val prop = Drule.plain_prop_of (Thm.transfer thy th);
+    val prop = Thm.plain_prop_of (Thm.transfer thy th);
     val rel = Logic.dest_classrel prop handle TERM _ => err ();
     val (c1, c2) = cert_classrel thy rel handle TYPE _ => err ();
   in
@@ -226,7 +226,7 @@
 fun add_arity th thy =
   let
     fun err () = raise THM ("add_arity: malformed type arity", 0, [th]);
-    val prop = Drule.plain_prop_of (Thm.transfer thy th);
+    val prop = Thm.plain_prop_of (Thm.transfer thy th);
     val (t, Ss, c) = Logic.dest_arity prop handle TERM _ => err ();
     val _ = if map (Sign.certify_sort thy) Ss = Ss then () else err ();
   in
diff -r 0b08f218f260 -r 290454649b8c src/Pure/variable.ML
--- a/src/Pure/variable.ML	Sun Apr 15 14:31:44 2007 +0200
+++ b/src/Pure/variable.ML	Sun Apr 15 14:31:47 2007 +0200
@@ -206,7 +206,7 @@
 
 val declare_prf = Proofterm.fold_proof_terms declare_internal (declare_internal o Logic.mk_type);
 
-val declare_thm = Drule.fold_terms declare_internal;
+val declare_thm = Thm.fold_terms declare_internal;
 fun thm_context th = declare_thm th (ProofContext.init (Thm.theory_of_thm th));
 
 
@@ -444,7 +444,7 @@
 
 fun focus_subgoal i st =
   let
-    val all_vars = Drule.fold_terms Term.add_vars st [];
+    val all_vars = Thm.fold_terms Term.add_vars st [];
     val no_binds = map (fn (xi, _) => (xi, NONE)) all_vars;
   in
     add_binds no_binds #>