# HG changeset patch
# User wenzelm
# Date 1011297738 -3600
# Node ID 5472afdd3bd333b2483c8e18df397d4c629d48f6
# Parent  f7e2d0d32ea7f03358d91d2defe875edca88c8ce
MetaSimplifier.rewrite_term replaces slow Tactic.rewrite_cterm;
RuleCases.make interface based on term instead of thm;

diff -r f7e2d0d32ea7 -r 5472afdd3bd3 src/Provers/induct_method.ML
--- a/src/Provers/induct_method.ML	Thu Jan 17 21:01:17 2002 +0100
+++ b/src/Provers/induct_method.ML	Thu Jan 17 21:02:18 2002 +0100
@@ -48,8 +48,7 @@
           let
             val cx = cert x;
             val {T = xT, sign, ...} = Thm.rep_cterm cx;
-            val orig_ct = cert t;
-            val ct = tune orig_ct;
+            val ct = cert (tune t);
           in
             if Sign.typ_instance sign (#T (Thm.rep_cterm ct), xT) then Some (cx, ct)
             else raise ERROR_MESSAGE (Pretty.string_of (Pretty.block
@@ -81,7 +80,7 @@
 fun resolveq_cases_tac make ruleq i st =
   ruleq |> Seq.map (fn (rule, (cases, facts)) =>
     (Method.insert_tac facts THEN' Tactic.rtac rule) i st
-    |> Seq.map (rpair (make rule cases)))
+    |> Seq.map (rpair (make (Thm.sign_of_thm rule, Thm.prop_of rule) cases)))
   |> Seq.flat;
 
 fun find_casesT ctxt ((Some t :: _) :: _) = InductAttrib.find_casesT ctxt (fastype_of t)
@@ -138,19 +137,25 @@
 
 (* atomize and rulify *)
 
-fun atomize_cterm ct =
-  Thm.cterm_fun (ObjectLogic.drop_judgment (#sign (Thm.rep_cterm ct)))
-    (Tactic.rewrite_cterm true Data.atomize ct);
+fun atomize_term sg =
+  ObjectLogic.drop_judgment sg o MetaSimplifier.rewrite_term sg Data.atomize;
+
+fun rulified_term thm =
+  let val sg = Thm.sign_of_thm thm in
+    Thm.prop_of thm
+    |> MetaSimplifier.rewrite_term sg Data.rulify1
+    |> MetaSimplifier.rewrite_term sg Data.rulify2
+    |> pair sg
+  end;
 
 val atomize_tac = Tactic.rewrite_goal_tac Data.atomize;
-val rulify = Tactic.simplify true Data.rulify2 o Tactic.simplify true Data.rulify1;
 
 val rulify_tac =
   Tactic.rewrite_goal_tac Data.rulify1 THEN'
   Tactic.rewrite_goal_tac Data.rulify2 THEN'
   Tactic.norm_hhf_tac;
 
-val localize = Tactic.norm_hhf o Tactic.simplify false Data.localize;
+val localize = Tactic.norm_hhf_rule o Tactic.simplify false Data.localize;
 
 
 (* imp_intr --- limited to atomic prems *)
@@ -226,7 +231,9 @@
   ruleq |> Seq.map (fn (rule, (cases, k, more_facts)) => st
     |> (Method.insert_tac more_facts THEN' atomize_tac) i
     |> Seq.map (fn st' => divinate_inst (internalize k rule) i st' |> Seq.map (fn rule' =>
-          st' |> Tactic.rtac rule' i |> Seq.map (rpair (make (rulify rule') cases))) |> Seq.flat)
+          st' |> Tactic.rtac rule' i
+          |> Seq.map (rpair (make (rulified_term rule') cases)))
+      |> Seq.flat)
     |> Seq.flat)
   |> Seq.flat;
 
@@ -263,7 +270,7 @@
       if null insts then r
       else (align_right "Rule has fewer conclusions than arguments given"
           (Data.dest_concls (Thm.concl_of r)) insts
-        |> (flat o map (prep_inst align_right cert atomize_cterm))
+        |> (flat o map (prep_inst align_right cert (atomize_term sg)))
         |> Drule.cterm_instantiate) r);
 
     val ruleq =