1 signature QUOTIENT_INFO =

     1 signature QUOTIENT_INFO =

     2 sig

     2 sig

     3   exception NotFound

     3   exception NotFound

     4 

     4 

     5   type maps_info = {mapfun: string, relmap: string}

     5   type maps_info = {mapfun: string, relmap: string}

     6   val maps_lookup: theory -> string -> maps_info     (* raises NotFound *)

     7   val maps_lookup: theory -> string -> maps_info     (* raises NotFound *)

     7   val maps_update_thy: string -> maps_info -> theory -> theory    

     8   val maps_update_thy: string -> maps_info -> theory -> theory    

     8   val maps_update: string -> maps_info -> Proof.context -> Proof.context     

     9   val maps_update: string -> maps_info -> Proof.context -> Proof.context     

     9   val print_mapsinfo: Proof.context -> unit

    10   val print_mapsinfo: Proof.context -> unit

    10 

    11 

    74 structure MapsData = Theory_Data

    75 structure MapsData = Theory_Data

    75   (type T = maps_info Symtab.table

    76   (type T = maps_info Symtab.table

    76    val empty = Symtab.empty

    77    val empty = Symtab.empty

    77    val extend = I

    78    val extend = I

    78    val merge = Symtab.merge (K true))

    79    val merge = Symtab.merge (K true))

    79 

    85 

    80 fun maps_lookup thy s = 

    86 fun maps_lookup thy s = 

    81   case (Symtab.lookup (MapsData.get thy) s) of

    87   case (Symtab.lookup (MapsData.get thy) s) of

    82     SOME map_fun => map_fun

    88     SOME map_fun => map_fun

    83   | NONE => raise NotFound

    89   | NONE => raise NotFound