src/Provers/induct_method.ML

--- a/src/Provers/induct_method.ML	Fri Feb 20 14:22:51 2004 +0100
+++ b/src/Provers/induct_method.ML	Sat Feb 21 08:43:08 2004 +0100
@@ -111,7 +111,7 @@
 
     fun prep_rule (th, (cases, n)) = Seq.map (apsnd (rpair (drop (n, facts))) o rpair cases)
       (Method.multi_resolves (take (n, facts)) [th]);
-  in resolveq_cases_tac (RuleCases.make (if is_open then None else Some 0) None) (Seq.flat (Seq.map prep_rule ruleq)) end;
+  in resolveq_cases_tac (RuleCases.make is_open None) (Seq.flat (Seq.map prep_rule ruleq)) end;
 
 in
 
@@ -225,24 +225,15 @@
 
 fun internalize k th = if k > 0 then internalize (k - 1) (imp_intr k th) else th;
 
-fun nof_params i st =
-  let val Bi = RuleCases.hhf_nth_subgoal (sign_of_thm st) (i,prop_of st)
-  in length(Logic.strip_params Bi) end
-  handle TERM("strip_prems",_) => 0 (* in case i is out of range *)
-
 fun resolveq_cases_tac' make is_open ruleq i st =
-  let val n = nof_params i st
-      val mk = make (if is_open then None else Some n)
-  in
   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 (mk (Some (Thm.prop_of rule')) (rulified_term rule') cases)))
+          |> Seq.map (rpair (make is_open (Some (Thm.prop_of rule')) (rulified_term rule') cases)))
       |> Seq.flat)
     |> Seq.flat)
-  |> Seq.flat
-  end;
+  |> Seq.flat;
 
 infix 1 THEN_ALL_NEW_CASES;