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