# HG changeset patch
# User wenzelm
# Date 1136633185 -3600
# Node ID 8f25a0f7f446e1d311177c0cf450ec8a5b94aa26
# Parent  b248754b60bc704671979fa06850234e544d4049
RuleCases.make_common/nested;

diff -r b248754b60bc -r 8f25a0f7f446 src/Provers/induct_method.ML
--- a/src/Provers/induct_method.ML	Sat Jan 07 12:26:23 2006 +0100
+++ b/src/Provers/induct_method.ML	Sat Jan 07 12:26:25 2006 +0100
@@ -94,7 +94,7 @@
 (* make_cases *)
 
 fun make_cases is_open rule =
-  RuleCases.make is_open NONE (Thm.theory_of_thm rule, Thm.prop_of rule);
+  RuleCases.make_common is_open (Thm.theory_of_thm rule, Thm.prop_of rule);
 
 fun warn_open true = warning "Encountered open rule cases -- deprecated"
   | warn_open false = ();
@@ -398,7 +398,8 @@
           |> tap (trace_rules ctxt InductAttrib.inductN o map #2)
           |> Seq.of_list |> Seq.maps (Seq.try inst_rule));
 
-    fun rule_cases rule = RuleCases.make is_open (SOME (Thm.prop_of rule)) (rulified_term rule);
+    fun rule_cases rule =
+      RuleCases.make_nested is_open (Thm.prop_of rule) (rulified_term rule);
   in
     (fn i => fn st =>
       ruleq