# HG changeset patch
# User kuncar
# Date 1353687852 -3600
# Node ID 2006c50172c92832913b80984d0562027412b438
# Parent  7017471769523165f5fbcb2c7fbc8a8fcce56cda
generate correct names

diff -r 701747176952 -r 2006c50172c9 src/HOL/Tools/Quotient/quotient_type.ML
--- a/src/HOL/Tools/Quotient/quotient_type.ML	Fri Nov 23 15:53:24 2012 +0100
+++ b/src/HOL/Tools/Quotient/quotient_type.ML	Fri Nov 23 17:24:12 2012 +0100
@@ -101,8 +101,8 @@
       | _ => error "unsupported equivalence theorem"
       )
     val def_term = Abs ("x", rty, Abs ("y", qty, Abs_body));
-    val qty_name = (fst o dest_Type) qty
-    val cr_rel_name = Binding.prefix_name "cr_" (Binding.qualified_name qty_name)  
+    val qty_name = (Binding.name o Long_Name.base_name o fst o dest_Type) qty
+    val cr_rel_name = Binding.prefix_name "cr_" qty_name
     val (fixed_def_term, lthy') = yield_singleton (Variable.importT_terms) def_term lthy
     val ((_, (_ , def_thm)), lthy'') =
       Local_Theory.define ((cr_rel_name, NoSyn), ((Thm.def_binding cr_rel_name, []), fixed_def_term)) lthy'
@@ -115,8 +115,8 @@
     val (_ $ _ $ abs_fun $ _) = (HOLogic.dest_Trueprop o prop_of) quot3_thm
     val (T_def, lthy') = define_cr_rel equiv_thm abs_fun lthy
     val (rty, qty) = (dest_funT o fastype_of) abs_fun
-    val qty_name = (fst o dest_Type) qty
-    val quotient_thm_name = Binding.prefix_name "Quotient_" (Binding.qualified_name qty_name) 
+    val qty_name = (Binding.name o Long_Name.base_name o fst o dest_Type) qty
+    val quotient_thm_name = Binding.prefix_name "Quotient_" qty_name
     val (reflp_thm, quot_thm) = (case (HOLogic.dest_Trueprop o prop_of) equiv_thm of
       Const (@{const_name equivp}, _) $ _ =>
         (SOME (equiv_thm RS @{thm equivp_reflp2}),