Thm.plain_prop_of;

--- a/src/Pure/Tools/codegen_data.ML	Sun Apr 15 14:32:04 2007 +0200
+++ b/src/Pure/Tools/codegen_data.ML	Sun Apr 15 14:32:05 2007 +0200
@@ -113,7 +113,7 @@
 fun add_drop_redundant thm (sels, dels) =
   let
     val thy = Thm.theory_of_thm thm;
-    val args_of = snd o strip_comb o fst o Logic.dest_equals o Drule.plain_prop_of;
+    val args_of = snd o strip_comb o fst o Logic.dest_equals o Thm.plain_prop_of;
     val args = args_of thm;
     fun matches [] _ = true
       | matches (Var _ :: xs) [] = matches xs []
@@ -783,7 +783,7 @@
             |> map (CodegenFunc.expand_eta ~1 o snd)
         | NONE => []
     fun drop_refl thy = filter_out (is_equal o Term.fast_term_ord o Logic.dest_equals
-      o ObjectLogic.drop_judgment thy o Drule.plain_prop_of);
+      o ObjectLogic.drop_judgment thy o Thm.plain_prop_of);
     val funcs = case get_funcs thy const
      of [] => get_prim_def_funcs const
     | funcs => funcs

--- a/src/Pure/Tools/codegen_func.ML	Sun Apr 15 14:32:04 2007 +0200
+++ b/src/Pure/Tools/codegen_func.ML	Sun Apr 15 14:32:05 2007 +0200
@@ -68,10 +68,10 @@
 (* making defining equations *)
 
 val typ_func = lift_thm_thy (fn thy => snd o dest_Const o fst o strip_comb
-  o fst o Logic.dest_equals o ObjectLogic.drop_judgment thy o Drule.plain_prop_of);
+  o fst o Logic.dest_equals o ObjectLogic.drop_judgment thy o Thm.plain_prop_of);
 
 val dest_func = lift_thm_thy (fn thy => apfst dest_Const o strip_comb
-  o fst o Logic.dest_equals o ObjectLogic.drop_judgment thy o Drule.plain_prop_of
+  o fst o Logic.dest_equals o ObjectLogic.drop_judgment thy o Thm.plain_prop_of
   o Drule.fconv_rule Drule.beta_eta_conversion);
 
 val mk_head = lift_thm_thy (fn thy => fn thm =>
@@ -132,7 +132,7 @@
 fun expand_eta k thm =
   let
     val thy = Thm.theory_of_thm thm;
-    val (lhs, rhs) = (Logic.dest_equals o Drule.plain_prop_of) thm;
+    val (lhs, rhs) = (Logic.dest_equals o Thm.plain_prop_of) thm;
     val (head, args) = strip_comb lhs;
     val l = if k = ~1
       then (length o fst o strip_abs) rhs
@@ -176,7 +176,7 @@
 fun norm_args thms =
   let
     val num_args_of = length o snd o strip_comb o fst o Logic.dest_equals;
-    val k = fold (curry Int.max o num_args_of o Drule.plain_prop_of) thms 0;
+    val k = fold (curry Int.max o num_args_of o Thm.plain_prop_of) thms 0;
   in
     thms
     |> map (expand_eta k)

--- a/src/Pure/Tools/codegen_funcgr.ML	Sun Apr 15 14:32:04 2007 +0200
+++ b/src/Pure/Tools/codegen_funcgr.ML	Sun Apr 15 14:32:05 2007 +0200
@@ -72,7 +72,7 @@
 
 fun fold_consts f thms =
   thms
-  |> maps (op :: o swap o apfst (snd o strip_comb) o Logic.dest_equals o Drule.plain_prop_of)
+  |> maps (op :: o swap o apfst (snd o strip_comb) o Logic.dest_equals o Thm.plain_prop_of)
   |> (fold o fold_aterms) (fn Const c => f c | _ => I);
 
 fun consts_of (const, []) = []

--- a/src/Pure/Tools/compute.ML	Sun Apr 15 14:32:04 2007 +0200
+++ b/src/Pure/Tools/compute.ML	Sun Apr 15 14:32:05 2007 +0200
@@ -163,7 +163,7 @@
 
         fun thm2rule table invtable ccount th =
             let
-                val prop = Drule.plain_prop_of th
+                val prop = Thm.plain_prop_of th
                   handle THM _ => raise (Make "theorems must be plain propositions")
                 val (a, b) = Logic.dest_equals prop
                   handle TERM _ => raise (Make "theorems must be meta-level equations")