# HG changeset patch
# User Christian Urban <urbanc@in.tum.de>
# Date 1258024053 -3600
# Node ID 4cf79f70efeca5c820447b5ae534f30690fd53f3
# Parent  77fc6f3c0343af306c58c318309cb0e7759ec3c6
looking up data in quot_info works now (needs qualified string)

diff -r 77fc6f3c0343 -r 4cf79f70efec IntEx.thy
--- a/IntEx.thy	Thu Nov 12 02:54:40 2009 +0100
+++ b/IntEx.thy	Thu Nov 12 12:07:33 2009 +0100
@@ -134,6 +134,8 @@
   lift_thm lthy qty ty_name rsp_thms defs t
 *}
 
+print_quotients
+
 ML {* lift_thm_my_int @{context} @{thm plus_sym_pre} *}
 
 lemma plus_assoc_pre:
diff -r 77fc6f3c0343 -r 4cf79f70efec quotient.ML
--- a/quotient.ML	Thu Nov 12 02:54:40 2009 +0100
+++ b/quotient.ML	Thu Nov 12 12:07:33 2009 +0100
@@ -146,7 +146,8 @@
   val quotient_thm_name = Binding.prefix_name "QUOTIENT_" qty_name
 
   (* storing the quot-info *)
-  val lthy3 = quotdata_update (Binding.str_of qty_name) 
+  val qty_str = fst (dest_Type abs_ty)		  
+  val lthy3 = quotdata_update qty_str 
                                 (Logic.varifyT abs_ty, Logic.varifyT rty, rel, equiv_thm) lthy2
 
   (* interpretation *)
diff -r 77fc6f3c0343 -r 4cf79f70efec quotient_def.ML
--- a/quotient_def.ML	Thu Nov 12 02:54:40 2009 +0100
+++ b/quotient_def.ML	Thu Nov 12 12:07:33 2009 +0100
@@ -138,7 +138,7 @@
 
   val ((trm, thm), lthy') = define nconst_bname mx attr absrep_trm lthy
 
-  val nconst_str = Binding.str_of nconst_bname
+  val nconst_str = Binding.name_of nconst_bname
   val qc_info = {qconst = trm, rconst = rhs}
   val lthy'' = qconsts_update nconst_str qc_info lthy'
 in