Tactic.rewrite_cterm;

--- a/src/HOL/Tools/inductive_package.ML	Mon Oct 15 20:34:44 2001 +0200
+++ b/src/HOL/Tools/inductive_package.ML	Mon Oct 15 20:35:10 2001 +0200
@@ -295,7 +295,7 @@
 val all_not_allowed = 
     "Introduction rule must not have a leading \"!!\" quantifier";
 
-val atomize_cterm = rewrite_cterm true inductive_atomize;
+val atomize_cterm = Tactic.rewrite_cterm true inductive_atomize;
 
 in
 

--- a/src/Provers/induct_method.ML	Mon Oct 15 20:34:44 2001 +0200
+++ b/src/Provers/induct_method.ML	Mon Oct 15 20:35:10 2001 +0200
@@ -147,11 +147,11 @@
 local
 
 fun atomize_cterm ct =
-  Thm.cterm_fun
-    (ObjectLogic.drop_judgment (#sign (Thm.rep_cterm ct))) (rewrite_cterm true Data.atomize ct);
+  Thm.cterm_fun (ObjectLogic.drop_judgment (#sign (Thm.rep_cterm ct)))
+    (Tactic.rewrite_cterm true Data.atomize ct);
 
 val atomize_tac = Tactic.rewrite_goal_tac Data.atomize;
-val rulify_cterm = rewrite_cterm true Data.rulify2 o rewrite_cterm true Data.rulify1;
+val rulify_cterm = Tactic.rewrite_cterm true Data.rulify2 o Tactic.rewrite_cterm true Data.rulify1;
 
 val rulify_tac =
   Tactic.rewrite_goal_tac Data.rulify1 THEN'