src/Pure/Isar/rule_cases.ML

--- a/src/Pure/Isar/rule_cases.ML	Sat May 30 19:29:21 2015 +0200
+++ b/src/Pure/Isar/rule_cases.ML	Sat May 30 20:21:53 2015 +0200
@@ -421,7 +421,7 @@
     fun rename_prems prop =
       let val (As, C) = Logic.strip_horn prop
       in Logic.list_implies (map rename As, C) end;
-  in Thm.equal_elim (Thm.reflexive (Drule.cterm_fun rename_prems (Thm.cprop_of rule))) rule end;
+  in Thm.renamed_prop (rename_prems (Thm.prop_of rule)) rule end;