when applying induction rules, remove names of assumptions that come
authornipkow
Fri Sep 16 09:18:15 2011 +0200 (2011-09-16)
changeset 44942a05ab4d803f2
parent 44937 22c0857b8aab
child 44943 b62559f085bc
when applying induction rules, remove names of assumptions that come
with the rule in case the rule is transformed by the simplifier due to
instantiations
src/Tools/induct.ML
     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