Mercurial Mercurial > hg > nominal2 / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
fixed problem with maps_update
authorChristian Urban <urbanc@in.tum.de>
Mon, 02 Nov 2009 09:47:49 +0100
changeset 256 53d7477a1f94
parent 255 264c7b9d19f4
child 257 68bd5c2a1b96
fixed problem with maps_update
quotient.ML file | annotate | diff | comparison | revisions 
--- 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))
nominal2