# HG changeset patch
# User wenzelm
# Date 1003170910 -7200
# Node ID a08b62908caa868bf911996cb5644fb41a868a5b
# Parent  d17ee22412577982859d1135368b9d3bcb38e2f8
Tactic.rewrite_cterm;

diff -r d17ee2241257 -r a08b62908caa src/HOL/Tools/inductive_package.ML
--- 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
 
diff -r d17ee2241257 -r a08b62908caa src/Provers/induct_method.ML
--- 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'