quotient_info.ML
changeset 321 f46dc0ca08c3
parent 320 7d3d86beacd6
child 322 d741ccea80d3
--- a/quotient_info.ML	Fri Nov 20 13:03:01 2009 +0100
+++ b/quotient_info.ML	Sat Nov 21 02:49:39 2009 +0100
@@ -20,7 +20,7 @@
   val qconsts_transfer: morphism -> qconsts_info -> qconsts_info
   val qconsts_lookup: theory -> string -> qconsts_info option
   val qconsts_update_thy: string -> qconsts_info -> theory -> theory    
-  val qconsts_update_generic: string -> qconsts_info -> Context.generic -> Context.generic 
+  val qconsts_update_gen: string -> qconsts_info -> Context.generic -> Context.generic 
   val print_qconstinfo: Proof.context -> unit
 end;
 
@@ -147,7 +147,7 @@
 val qconsts_lookup = Symtab.lookup o QConstsData.get
 
 fun qconsts_update_thy k qcinfo = QConstsData.map (Symtab.update (k, qcinfo))
-fun qconsts_update_generic k qcinfo = 
+fun qconsts_update_gen k qcinfo = 
       Context.mapping (qconsts_update_thy k qcinfo) I
 
 fun print_qconstinfo ctxt =