1.1 --- a/src/Provers/induct_method.ML	Mon Nov 12 23:28:49 2001 +0100
     1.2 +++ b/src/Provers/induct_method.ML	Mon Nov 12 23:30:16 2001 +0100
     1.3 @@ -150,7 +150,7 @@
     1.4    Tactic.rewrite_goal_tac Data.rulify2 THEN'
     1.5    Tactic.norm_hhf_tac;
     1.6  
     1.7 -val localize_concl = Tactic.simplify false [Thm.symmetric Data.local_imp_def];
     1.8 +val localize = Tactic.simplify false [Thm.symmetric Data.local_imp_def];
     1.9  
    1.10  
    1.11  (* imp_intr --- limited to atomic prems *)
    1.12 @@ -225,7 +225,7 @@
    1.13    ruleq |> Seq.map (fn (rule, (cases, k, more_facts)) => st
    1.14      |> (Method.insert_tac more_facts THEN' atomize_tac) i
    1.15      |> Seq.map (fn st' => divinate_inst (internalize k rule) i st' |> Seq.map (fn rule' =>
    1.16 -          (PolyML.print st') |> Tactic.rtac (PolyML.print rule') i |> Seq.map (rpair (make (rulify rule') cases))) |> Seq.flat)
    1.17 +          st' |> Tactic.rtac rule' i |> Seq.map (rpair (make (rulify rule') cases))) |> Seq.flat)
    1.18      |> Seq.flat)
    1.19    |> Seq.flat;
    1.20  
    1.21 @@ -254,24 +254,26 @@
    1.22      val sg = ProofContext.sign_of ctxt;
    1.23      val cert = Thm.cterm_of sg;
    1.24  
    1.25 -    fun inst_rule r =
    1.26 -      if null insts then RuleCases.add r
    1.27 +    fun rule_versions r = Seq.cons (r, Seq.filter (not o curry eq_thm r)
    1.28 +        (Seq.make (fn () => Some (localize r, Seq.empty))))
    1.29 +      |> Seq.map (rpair (RuleCases.get r));
    1.30 +
    1.31 +    val inst_rule = apfst (fn r =>
    1.32 +      if null insts then r
    1.33        else (align_right "Rule has fewer conclusions than arguments given"
    1.34            (Data.dest_concls (Thm.concl_of r)) insts
    1.35          |> (flat o map (prep_inst align_right cert atomize_cterm))
    1.36 -        |> Drule.cterm_instantiate) r |> rpair (RuleCases.get r);
    1.37 +        |> Drule.cterm_instantiate) r);
    1.38  
    1.39      val ruleq =
    1.40        (case opt_rule of
    1.41          None =>
    1.42            let val rules = find_inductS ctxt facts @ find_inductT ctxt insts in
    1.43 -            if null rules then error "Unable to figure out induct rule" else ();
    1.44 +            conditional (null rules) (fn () => error "Unable to figure out induct rule");
    1.45              Method.trace ctxt rules;
    1.46 -            Seq.flat (Seq.map (Seq.APPEND (Seq.try inst_rule,
    1.47 -              Seq.try (inst_rule o localize_concl))) (Seq.of_list rules))
    1.48 +            rules |> Seq.THEN (Seq.of_list, Seq.THEN (rule_versions, Seq.try inst_rule))
    1.49            end
    1.50 -      | Some r => Seq.make (fn () => Some (inst_rule r,
    1.51 -          Seq.make (fn () => Some (inst_rule (localize_concl r), Seq.empty)))));
    1.52 +      | Some r => r |> Seq.THEN (rule_versions, Seq.single o inst_rule));
    1.53  
    1.54      fun prep_rule (th, (cases, n)) =
    1.55        Seq.map (rpair (cases, n - length facts, drop (n, facts)))