# HG changeset patch
# User kuncar
# Date 1334849494 -7200
# Node ID 5c17ef8feac7ab3d30e99ccfba9aaf542f55ba24
# Parent  06dde48a1503ee06da7ecc26943210b970e0335f
use tnames for bound variables in rsp thms

diff -r 06dde48a1503 -r 5c17ef8feac7 src/HOL/Tools/Lifting/lifting_def.ML
--- a/src/HOL/Tools/Lifting/lifting_def.ML	Thu Apr 19 17:49:08 2012 +0200
+++ b/src/HOL/Tools/Lifting/lifting_def.ML	Thu Apr 19 17:31:34 2012 +0200
@@ -250,7 +250,20 @@
     Object_Logic.rulify(eq_thm RS Drule.equal_elim_rule2)
   end
 
+fun rename_to_tnames ctxt term =
+  let
+    fun all_typs (Const ("all", _) $ Abs (_, T, t)) = T :: all_typs t
+      | all_typs _ = []
 
+    fun rename (Const ("all", T1) $ Abs (_, T2, t)) (new_name :: names) = 
+        (Const ("all", T1) $ Abs (new_name, T2, rename t names)) 
+      | rename t _ = t
+
+    val (fixed_def_t, _) = yield_singleton (Variable.importT_terms) term ctxt
+    val new_names = Datatype_Prop.make_tnames (all_typs fixed_def_t)
+  in
+    rename term new_names
+  end
 
 fun lift_def_cmd (raw_var, rhs_raw) lthy =
   let
@@ -279,7 +292,8 @@
     val readable_rsp_thm_eq = mk_readable_rsp_thm_eq internal_rsp_tm lthy'
     val maybe_proven_rsp_thm = try_to_prove_refl readable_rsp_thm_eq
     val (readable_rsp_tm, _) = Logic.dest_implies (prop_of readable_rsp_thm_eq)
-  
+    val readable_rsp_tm_tnames = rename_to_tnames lthy' readable_rsp_tm
+
     fun after_qed thm_list lthy = 
       let
         val internal_rsp_thm =
@@ -294,7 +308,7 @@
   in
     case maybe_proven_rsp_thm of
       SOME _ => Proof.theorem NONE after_qed [] lthy'
-      | NONE =>  Proof.theorem NONE after_qed [[(readable_rsp_tm,[])]] lthy'
+      | NONE =>  Proof.theorem NONE after_qed [[(readable_rsp_tm_tnames,[])]] lthy'
   end
 
 fun quot_thm_err ctxt (rty, qty) pretty_msg =