# HG changeset patch
# User wenzelm
# Date 1136633305 -3600
# Node ID 05a5e950d5f1cb942d4ab21d3cc87f041060abc4
# Parent  b026652ede90d629951ffa5ac176217c9f3a17c1
RuleCases.make_nested;

diff -r b026652ede90 -r 05a5e950d5f1 src/HOL/Nominal/nominal_induct.ML
--- a/src/HOL/Nominal/nominal_induct.ML	Sat Jan 07 12:26:35 2006 +0100
+++ b/src/HOL/Nominal/nominal_induct.ML	Sat Jan 07 12:28:25 2006 +0100
@@ -93,7 +93,7 @@
     val finish_rule = PolyML.print #>
       split_all_tuples
       #> rename_params_rule true (map (ProofContext.revert_skolem defs_ctxt o fst) avoiding) #> PolyML.print;
-    fun rule_cases r = RuleCases.make true (SOME (Thm.prop_of r)) (InductMethod.rulified_term r);
+    fun rule_cases r = RuleCases.make_nested true (Thm.prop_of r) (InductMethod.rulified_term r);
   in
     (fn i => fn st =>
       rules