--- 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'
--- 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;
--- 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
--- 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;
--- 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
--- 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
--- 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 #>