tuned -- more direct Thm.renamed_prop;

--- a/src/HOL/Nominal/nominal_induct.ML	Sat May 30 19:29:21 2015 +0200
+++ b/src/HOL/Nominal/nominal_induct.ML	Sat May 30 20:21:53 2015 +0200
@@ -76,7 +76,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;
 
 
 (* nominal_induct_tac *)

--- 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;
 
 
 

--- a/src/Pure/drule.ML	Sat May 30 19:29:21 2015 +0200
+++ b/src/Pure/drule.ML	Sat May 30 20:21:53 2015 +0200
@@ -829,19 +829,16 @@
 fun rename_bvars [] thm = thm
   | rename_bvars vs thm =
       let
-        val thy = Thm.theory_of_thm thm;
-        fun ren (Abs (x, T, t)) = Abs (AList.lookup (op =) vs x |> the_default x, T, ren t)
-          | ren (t $ u) = ren t $ ren u
-          | ren t = t;
-      in Thm.equal_elim (Thm.reflexive (Thm.global_cterm_of thy (ren (Thm.prop_of thm)))) thm end;
+        fun rename (Abs (x, T, t)) = Abs (AList.lookup (op =) vs x |> the_default x, T, rename t)
+          | rename (t $ u) = rename t $ rename u
+          | rename a = a;
+      in Thm.renamed_prop (rename (Thm.prop_of thm)) thm end;
 
 
 (* renaming in left-to-right order *)
 
 fun rename_bvars' xs thm =
   let
-    val thy = Thm.theory_of_thm thm;
-    val prop = Thm.prop_of thm;
     fun rename [] t = ([], t)
       | rename (x' :: xs) (Abs (x, T, t)) =
           let val (xs', t') = rename xs t
@@ -849,12 +846,12 @@
       | rename xs (t $ u) =
           let
             val (xs', t') = rename xs t;
-            val (xs'', u') = rename xs' u
+            val (xs'', u') = rename xs' u;
           in (xs'', t' $ u') end
       | rename xs t = (xs, t);
   in
-    (case rename xs prop of
-      ([], prop') => Thm.equal_elim (Thm.reflexive (Thm.global_cterm_of thy prop')) thm
+    (case rename xs (Thm.prop_of thm) of
+      ([], prop') => Thm.renamed_prop prop' thm
     | _ => error "More names than abstractions in theorem")
   end;
 

--- a/src/Tools/induct.ML	Sat May 30 19:29:21 2015 +0200
+++ b/src/Tools/induct.ML	Sat May 30 20:21:53 2015 +0200
@@ -617,11 +617,10 @@
               (case filter (fn x' => x' = x) xs of
                 [] => xs | [_] => xs | _ => index 1 xs);
           in Logic.list_rename_params xs' A end;
-        fun rename_prop p =
-          let val (As, C) = Logic.strip_horn p
+        fun rename_prop prop =
+          let val (As, C) = Logic.strip_horn prop
           in Logic.list_implies (map rename_asm As, C) end;
-        val cp' = cterm_fun rename_prop (Thm.cprop_of thm);
-        val thm' = Thm.equal_elim (Thm.reflexive cp') thm;
+        val thm' = Thm.renamed_prop (rename_prop (Thm.prop_of thm)) thm;
       in [Rule_Cases.save thm thm'] end
   | special_rename_params _ _ ths = ths;