# HG changeset patch
# User wenzelm
# Date 1011297677 -3600
# Node ID f7e2d0d32ea7f03358d91d2defe875edca88c8ce
# Parent  4de06a8f67ef47ecf2eccd431ab85201445e7b2a
MetaSimplifier.rewrite_term replaces slow Tactic.rewrite_cterm;

diff -r 4de06a8f67ef -r f7e2d0d32ea7 src/HOL/Tools/inductive_package.ML
--- a/src/HOL/Tools/inductive_package.ML	Thu Jan 17 21:00:38 2002 +0100
+++ b/src/HOL/Tools/inductive_package.ML	Thu Jan 17 21:01:17 2002 +0100
@@ -296,7 +296,7 @@
 val all_not_allowed = 
     "Introduction rule must not have a leading \"!!\" quantifier";
 
-val atomize_cterm = Tactic.rewrite_cterm true inductive_atomize;
+fun atomize_term sg = MetaSimplifier.rewrite_term sg inductive_atomize;
 
 in
 
@@ -304,7 +304,7 @@
   let
     val concl = Logic.strip_imp_concl rule;
     val prems = Logic.strip_imp_prems rule;
-    val aprems = prems |> map (Thm.term_of o atomize_cterm o Thm.cterm_of sg);
+    val aprems = map (atomize_term sg) prems;
     val arule = Logic.list_implies (aprems, concl);
 
     fun check_prem (prem, aprem) =
@@ -324,7 +324,7 @@
   end;
 
 val rulify =
-  standard o Tactic.norm_hhf o
+  standard o Tactic.norm_hhf_rule o
   hol_simplify inductive_rulify2 o hol_simplify inductive_rulify1 o
   hol_simplify inductive_conj;