# HG changeset patch
# User wenzelm
# Date 1133360672 -3600
# Node ID af72dfc4b9f9d8a6cef5cccabfc5b96aeb24301c
# Parent  f7899cb24c7949bb1e1318211fab551bd05401b3
added rename_params_rule: recover orginal fresh names in subgoals/cases;

diff -r f7899cb24c79 -r af72dfc4b9f9 src/HOL/Nominal/nominal_induct.ML
--- a/src/HOL/Nominal/nominal_induct.ML	Wed Nov 30 15:03:15 2005 +0100
+++ b/src/HOL/Nominal/nominal_induct.ML	Wed Nov 30 15:24:32 2005 +0100
@@ -48,12 +48,24 @@
     |> Drule.cterm_instantiate (map (pairself (Thm.cterm_of thy)) subst)
   end;
 
-fun rename_params_prems xs rule =
+fun rename_params_rule internal xs rule =
   let
-    val cert = Thm.cterm_of (Thm.theory_of_thm rule);
-    val (As, C) = Logic.strip_horn (Thm.prop_of rule);
-    val prop = Logic.list_implies (map (curry Logic.list_rename_params xs) As, C);
-  in Thm.equal_elim (Thm.reflexive (cert prop)) rule end;
+    val tune =
+      if internal then Syntax.internal
+      else fn x => the_default x (try Syntax.dest_internal x);
+    val n = length xs;
+    fun rename prem =
+      let
+        val ps = Logic.strip_params prem;
+        val p = length ps;
+        val ys =
+          if p < n then []
+          else map (tune o #1) (Library.take (p - n, ps)) @ xs;
+      in Logic.list_rename_params (ys, prem) end;
+    fun rename_prems prop =
+      let val (As, C) = Logic.strip_horn (Thm.prop_of rule)
+      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;
 
 
 (* nominal_induct_tac *)
@@ -68,8 +80,8 @@
 
     val finish_rule =
       split_all_tuples
-      #> rename_params_prems (map (ProofContext.revert_skolem defs_ctxt o #1) fresh);
-    fun rule_cases r = RuleCases.make false (SOME (Thm.prop_of r)) (InductMethod.rulified_term r);
+      #> rename_params_rule true (map (ProofContext.revert_skolem defs_ctxt o #1) fresh);
+    fun rule_cases r = RuleCases.make true (SOME (Thm.prop_of r)) (InductMethod.rulified_term r);
   in
     (fn i => fn st =>
       rule
@@ -84,7 +96,7 @@
             InductMethod.guess_instance (finish_rule r) i st'
             |> Seq.maps (fn r' =>
               CASES (rule_cases r' cases)
-                (Tactic.rtac r' i THEN
+                (Tactic.rtac (rename_params_rule false [] r') i THEN
                   PRIMSEQ (ProofContext.exports defs_ctxt ctxt)) st'))))
     THEN_ALL_NEW_CASES InductMethod.rulify_tac
   end;