--- 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