# HG changeset patch
# User Christian Urban <urbanc@in.tum.de>
# Date 1257151669 -3600
# Node ID 53d7477a1f94da1a2a0e89abc006c8243a07d4c7
# Parent  264c7b9d19f4a3784db7dc4c32ae9a0d199e8c2f
fixed problem with maps_update

diff -r 264c7b9d19f4 -r 53d7477a1f94 quotient.ML
--- a/quotient.ML	Mon Nov 02 09:39:29 2009 +0100
+++ b/quotient.ML	Mon Nov 02 09:47:49 2009 +0100
@@ -6,7 +6,7 @@
   val mk_quotient_type_cmd: (((bstring * mixfix) * string) * string) list -> Proof.context -> Proof.state
   val define: binding * mixfix * term -> local_theory -> (term * thm) * local_theory
   val note: binding * thm -> local_theory -> thm * local_theory
-  val maps_lookup_thy: theory -> string -> maps_info option
+  val maps_lookup: theory -> string -> maps_info option
   val maps_update_thy: string -> maps_info -> theory -> theory    
   val maps_update: string -> maps_info -> Proof.context -> Proof.context                           
   val print_quotdata: Proof.context -> unit
@@ -32,7 +32,7 @@
    val extend = I
    fun merge _ = Symtab.merge (K true))
 
-val maps_lookup_thy = Symtab.lookup o MapsData.get
+val maps_lookup = Symtab.lookup o MapsData.get
 
 
 fun maps_update_thy k minfo = MapsData.map (Symtab.update (k, minfo))