diff -r 243a5ceaa088 -r 17ca92ab4660 Quot/quotient_info.ML
--- a/Quot/quotient_info.ML	Thu Feb 11 09:23:59 2010 +0100
+++ b/Quot/quotient_info.ML	Thu Feb 11 10:06:02 2010 +0100
@@ -13,8 +13,8 @@
   type maps_info = {mapfun: string, relmap: string}
   val maps_defined: theory -> string -> bool
   val maps_lookup: theory -> string -> maps_info     (* raises NotFound *)
-  val maps_update_thy: string -> maps_info -> theory -> theory    
-  val maps_update: string -> maps_info -> Proof.context -> Proof.context     
+  val maps_update_thy: string -> maps_info -> theory -> theory
+  val maps_update: string -> maps_info -> Proof.context -> Proof.context
   val print_mapsinfo: Proof.context -> unit
 
   type quotdata_info = {qtyp: typ, rtyp: typ, equiv_rel: term, equiv_thm: thm}
@@ -36,8 +36,8 @@
 
   val equiv_rules_get: Proof.context -> thm list
   val equiv_rules_add: attribute
-  val rsp_rules_get: Proof.context -> thm list  
-  val prs_rules_get: Proof.context -> thm list  
+  val rsp_rules_get: Proof.context -> thm list
+  val prs_rules_get: Proof.context -> thm list
   val id_simps_get: Proof.context -> thm list
   val quotient_rules_get: Proof.context -> thm list
   val quotient_rules_add: attribute
@@ -61,10 +61,10 @@
    val extend = I
    val merge = Symtab.merge (K true))
 
-fun maps_defined thy s = 
+fun maps_defined thy s =
   Symtab.defined (MapsData.get thy) s
 
-fun maps_lookup thy s = 
+fun maps_lookup thy s =
   case (Symtab.lookup (MapsData.get thy) s) of
     SOME map_fun => map_fun
   | NONE => raise NotFound
@@ -72,12 +72,12 @@
 fun maps_update_thy k minfo = MapsData.map (Symtab.update (k, minfo))
 fun maps_update k minfo = ProofContext.theory (maps_update_thy k minfo)
 
-fun maps_attribute_aux s minfo = Thm.declaration_attribute 
+fun maps_attribute_aux s minfo = Thm.declaration_attribute
   (fn _ => Context.mapping (maps_update_thy s minfo) (maps_update s minfo))
 
 (* attribute to be used in declare statements *)
-fun maps_attribute (ctxt, (tystr, (mapstr, relstr))) = 
-let  
+fun maps_attribute (ctxt, (tystr, (mapstr, relstr))) =
+let
   val thy = ProofContext.theory_of ctxt
   val tyname = Sign.intern_type thy tystr
   val mapname = Sign.intern_const thy mapstr
@@ -89,21 +89,21 @@
   maps_attribute_aux tyname {mapfun = mapname, relmap = relname}
 end
 
-val maps_attr_parser = 
+val maps_attr_parser =
   Args.context -- Scan.lift
-    ((Args.name --| OuterParse.$$$ "=") -- 
-      (OuterParse.$$$ "(" |-- Args.name --| OuterParse.$$$ "," -- 
+    ((Args.name --| OuterParse.$$$ "=") --
+      (OuterParse.$$$ "(" |-- Args.name --| OuterParse.$$$ "," --
         Args.name --| OuterParse.$$$ ")"))
 
 val _ = Context.>> (Context.map_theory
-  (Attrib.setup @{binding "map"} (maps_attr_parser >> maps_attribute) 
+  (Attrib.setup @{binding "map"} (maps_attr_parser >> maps_attribute)
     "declaration of map information"))
 
 fun print_mapsinfo ctxt =
 let
-  fun prt_map (ty_name, {mapfun, relmap}) = 
+  fun prt_map (ty_name, {mapfun, relmap}) =
     Pretty.block (Library.separate (Pretty.brk 2)
-      (map Pretty.str 
+      (map Pretty.str
         ["type:", ty_name,
         "map:", mapfun,
         "relation map:", relmap]))
@@ -111,11 +111,11 @@
   MapsData.get (ProofContext.theory_of ctxt)
   |> Symtab.dest
   |> map (prt_map)
-  |> Pretty.big_list "maps for type constructors:" 
+  |> Pretty.big_list "maps for type constructors:"
   |> Pretty.writeln
 end
 
- 
+
 (* info about quotient types *)
 type quotdata_info = {qtyp: typ, rtyp: typ, equiv_rel: term, equiv_thm: thm}
 
@@ -123,7 +123,7 @@
   (type T = quotdata_info Symtab.table
    val empty = Symtab.empty
    val extend = I
-   val merge = Symtab.merge (K true)) 
+   val merge = Symtab.merge (K true))
 
 fun transform_quotdata phi {qtyp, rtyp, equiv_rel, equiv_thm} =
   {qtyp = Morphism.typ phi qtyp,
@@ -160,7 +160,7 @@
   QuotData.get (ProofContext.theory_of ctxt)
   |> Symtab.dest
   |> map (prt_quot o snd)
-  |> Pretty.big_list "quotients:" 
+  |> Pretty.big_list "quotients:"
   |> Pretty.writeln
 end
 
@@ -223,7 +223,7 @@
   |> map snd
   |> flat
   |> map prt_qconst
-  |> Pretty.big_list "quotient constants:" 
+  |> Pretty.big_list "quotient constants:"
   |> Pretty.writeln
 end
 
@@ -266,7 +266,7 @@
 
 (* setup of the theorem lists *)
 
-val _ = Context.>> (Context.map_theory 
+val _ = Context.>> (Context.map_theory
   (EquivRules.setup #>
    RspRules.setup #>
    PrsRules.setup #>