# HG changeset patch
# User wenzelm
# Date 1004459421 -3600
# Node ID 324f69149895dc7c3531fe22a711bb0b1542abcf
# Parent  85141af30120af4b1db8dff6394be9a46db66c41
induct: cases are extracted from rulified rule;

diff -r 85141af30120 -r 324f69149895 src/Provers/induct_method.ML
--- a/src/Provers/induct_method.ML	Tue Oct 30 17:29:43 2001 +0100
+++ b/src/Provers/induct_method.ML	Tue Oct 30 17:30:21 2001 +0100
@@ -141,21 +141,13 @@
     (Tactic.rewrite_cterm true Data.atomize ct);
 
 val atomize_tac = Tactic.rewrite_goal_tac Data.atomize;
-val rulify_cterm = Tactic.rewrite_cterm true Data.rulify2 o Tactic.rewrite_cterm true Data.rulify1;
+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;
 
-fun rulify_cases sg cert =
-  let
-    val ruly = Thm.term_of o rulify_cterm o cert;
-    fun ruly_case {fixes, assumes, binds} =
-      {fixes = fixes, assumes = map ruly assumes,
-        binds = map (apsnd (apsome (ObjectLogic.drop_judgment sg o ruly))) binds};
-  in map (apsnd ruly_case) ooo RuleCases.make_raw end;
-
 
 (* join multi-rules *)
 
@@ -214,9 +206,8 @@
 fun resolveq_cases_tac' make ruleq i st =
   ruleq |> Seq.map (fn (rule, (cases, facts)) => st
     |> (Method.insert_tac facts THEN' atomize_tac) i
-    |> Seq.map (fn st' => divinate_inst rule i st'
-      |> Seq.map (fn rule' => st' |> Tactic.rtac rule' i |> Seq.map (rpair (make rule' cases)))
-      |> Seq.flat)
+    |> Seq.map (fn st' => divinate_inst rule i st' |> Seq.map (fn rule' =>
+        st' |> Tactic.rtac rule' i |> Seq.map (rpair (make (rulify rule') cases))) |> Seq.flat)
     |> Seq.flat)
   |> Seq.flat;
 
@@ -264,8 +255,7 @@
 
     fun prep_rule (th, (cases, n)) =
       Seq.map (rpair (cases, drop (n, facts))) (Method.multi_resolves (take (n, facts)) [th]);
-    val tac = resolveq_cases_tac' (rulify_cases sg cert open_parms)
-      (Seq.flat (Seq.map prep_rule ruleq));
+    val tac = resolveq_cases_tac' (RuleCases.make open_parms) (Seq.flat (Seq.map prep_rule ruleq));
   in tac THEN_ALL_NEW_CASES rulify_tac end;
 
 in