# HG changeset patch
# User kuncar
# Date 1334831290 -7200
# Node ID f3f0e06549c2b0771ce7c1c44b74c661c1415a8d
# Parent  cee347fe7ab1bff1dbf5713565539abdd40d2e14
create thm names correctly

diff -r cee347fe7ab1 -r f3f0e06549c2 src/HOL/Tools/Lifting/lifting_setup.ML
--- a/src/HOL/Tools/Lifting/lifting_setup.ML	Thu Apr 19 13:19:57 2012 +0200
+++ b/src/HOL/Tools/Lifting/lifting_setup.ML	Thu Apr 19 12:28:10 2012 +0200
@@ -97,7 +97,7 @@
     val transfer_attr = Attrib.internal (K Transfer.transfer_add)
     val (_, qty) = Lifting_Term.quot_thm_rty_qty quot_thm
     val induct_attr = Attrib.internal (K (Induct.induct_type (fst (dest_Type qty))))
-    val qty_name = (Binding.name o fst o dest_Type) qty
+    val qty_name = (Binding.name o Long_Name.base_name o fst o dest_Type) qty
     fun qualify suffix = Binding.qualified true suffix qty_name
     val lthy' = case maybe_reflp_thm of
       SOME reflp_thm => lthy
@@ -142,7 +142,7 @@
         [typedef_thm, T_def] MRSL @{thm typedef_to_Quotient}
 
     val (_, qty) = Lifting_Term.quot_thm_rty_qty quot_thm
-    val qty_name = (Binding.name o fst o dest_Type) qty
+    val qty_name = (Binding.name o Long_Name.base_name o fst o dest_Type) qty
     fun qualify suffix = Binding.qualified true suffix qty_name
 
     val lthy'' = case typedef_set of