src/Tools/induct.ML
changeset 44942 a05ab4d803f2
parent 44241 7943b69f0188
child 45014 0e847655b2d8
     1.1 --- a/src/Tools/induct.ML	Thu Sep 15 12:40:08 2011 -0400
     1.2 +++ b/src/Tools/induct.ML	Fri Sep 16 09:18:15 2011 +0200
     1.3 @@ -746,10 +746,16 @@
     1.4            |> tap (trace_rules ctxt inductN o map #2)
     1.5            |> Seq.of_list |> Seq.maps (Seq.try inst_rule));
     1.6  
     1.7 -    fun rule_cases ctxt rule =
     1.8 -      let val rule' = (if simp then simplified_rule ctxt else I)
     1.9 -        (Rule_Cases.internalize_params rule);
    1.10 -      in Rule_Cases.make_nested (Thm.prop_of rule') (rulified_term rule') end;
    1.11 +    fun rule_cases ctxt rule cases =
    1.12 +      let
    1.13 +        val rule' = Rule_Cases.internalize_params rule;
    1.14 +        val rule'' = (if simp then simplified_rule ctxt else I) rule';
    1.15 +        val nonames = map (fn ((cn,_),cls) => ((cn,[]),cls))
    1.16 +        val cases' =
    1.17 +          if Thm.eq_thm_prop (rule', rule'') then cases else nonames cases
    1.18 +      in Rule_Cases.make_nested (Thm.prop_of rule'') (rulified_term rule'')
    1.19 +           cases'
    1.20 +      end;
    1.21    in
    1.22      (fn i => fn st =>
    1.23        ruleq