# HG changeset patch
# User nipkow
# Date 1316157495 -7200
# Node ID a05ab4d803f2b8eab8c21f1022bcb3b0ca5ab690
# Parent  22c0857b8aab48518427dd8314192efa5a21002f
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

diff -r 22c0857b8aab -r a05ab4d803f2 src/Tools/induct.ML
--- a/src/Tools/induct.ML	Thu Sep 15 12:40:08 2011 -0400
+++ b/src/Tools/induct.ML	Fri Sep 16 09:18:15 2011 +0200
@@ -746,10 +746,16 @@
           |> tap (trace_rules ctxt inductN o map #2)
           |> Seq.of_list |> Seq.maps (Seq.try inst_rule));
 
-    fun rule_cases ctxt rule =
-      let val rule' = (if simp then simplified_rule ctxt else I)
-        (Rule_Cases.internalize_params rule);
-      in Rule_Cases.make_nested (Thm.prop_of rule') (rulified_term rule') end;
+    fun rule_cases ctxt rule cases =
+      let
+        val rule' = Rule_Cases.internalize_params rule;
+        val rule'' = (if simp then simplified_rule ctxt else I) rule';
+        val nonames = map (fn ((cn,_),cls) => ((cn,[]),cls))
+        val cases' =
+          if Thm.eq_thm_prop (rule', rule'') then cases else nonames cases
+      in Rule_Cases.make_nested (Thm.prop_of rule'') (rulified_term rule'')
+           cases'
+      end;
   in
     (fn i => fn st =>
       ruleq