src/HOL/Nominal/nominal_induct.ML
changeset 18610 05a5e950d5f1
parent 18583 96e1ef2f806f
child 19036 73782d21e855
     1.1 --- a/src/HOL/Nominal/nominal_induct.ML	Sat Jan 07 12:26:35 2006 +0100
     1.2 +++ b/src/HOL/Nominal/nominal_induct.ML	Sat Jan 07 12:28:25 2006 +0100
     1.3 @@ -93,7 +93,7 @@
     1.4      val finish_rule = PolyML.print #>
     1.5        split_all_tuples
     1.6        #> rename_params_rule true (map (ProofContext.revert_skolem defs_ctxt o fst) avoiding) #> PolyML.print;
     1.7 -    fun rule_cases r = RuleCases.make true (SOME (Thm.prop_of r)) (InductMethod.rulified_term r);
     1.8 +    fun rule_cases r = RuleCases.make_nested true (Thm.prop_of r) (InductMethod.rulified_term r);
     1.9    in
    1.10      (fn i => fn st =>
    1.11        rules