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