diff -r 139b257e10d2 -r 551eacf071d7 Quot/quotient_info.ML
--- a/Quot/quotient_info.ML	Tue Feb 09 14:32:37 2010 +0100
+++ b/Quot/quotient_info.ML	Tue Feb 09 15:28:15 2010 +0100
@@ -116,23 +116,23 @@
 end
 
 val maps_attr_parser = 
-      Args.context -- Scan.lift
-       ((Args.name --| OuterParse.$$$ "=") -- 
-         (OuterParse.$$$ "(" |-- Args.name --| OuterParse.$$$ "," -- 
-           Args.name --| OuterParse.$$$ ")"))
+  Args.context -- Scan.lift
+    ((Args.name --| OuterParse.$$$ "=") -- 
+      (OuterParse.$$$ "(" |-- Args.name --| OuterParse.$$$ "," -- 
+        Args.name --| OuterParse.$$$ ")"))
 
 val _ = Context.>> (Context.map_theory
-         (Attrib.setup @{binding "map"} (maps_attr_parser >> maps_attribute) 
-           "declaration of map information"))
+  (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}) = 
-      Pretty.block (Library.separate (Pretty.brk 2)
-        (map Pretty.str 
-          ["type:", ty_name,
-           "map:", mapfun,
-           "relation map:", relmap]))
+    Pretty.block (Library.separate (Pretty.brk 2)
+      (map Pretty.str 
+        ["type:", ty_name,
+        "map:", mapfun,
+        "relation map:", relmap]))
 in
   MapsData.get (ProofContext.theory_of ctxt)
   |> Symtab.dest
@@ -152,10 +152,10 @@
    val merge = Symtab.merge (K true)) 
 
 fun transform_quotdata phi {qtyp, rtyp, equiv_rel, equiv_thm} =
-    {qtyp = Morphism.typ phi qtyp,
-     rtyp = Morphism.typ phi rtyp,
-     equiv_rel = Morphism.term phi equiv_rel,
-     equiv_thm = Morphism.thm phi equiv_thm}
+  {qtyp = Morphism.typ phi qtyp,
+   rtyp = Morphism.typ phi rtyp,
+   equiv_rel = Morphism.term phi equiv_rel,
+   equiv_thm = Morphism.thm phi equiv_thm}
 
 fun quotdata_lookup_raw thy str = Symtab.lookup (QuotData.get thy) str
 
@@ -172,16 +172,16 @@
 
 fun print_quotinfo ctxt =
 let
-  fun prt_quot {qtyp, rtyp, equiv_rel, equiv_thm} = 
-      Pretty.block (Library.separate (Pretty.brk 2)
-          [Pretty.str "quotient type:", 
-           Syntax.pretty_typ ctxt qtyp,
-           Pretty.str "raw type:", 
-           Syntax.pretty_typ ctxt rtyp,
-           Pretty.str "relation:", 
-           Syntax.pretty_term ctxt equiv_rel,
-           Pretty.str "equiv. thm:", 
-           Syntax.pretty_term ctxt (prop_of equiv_thm)])
+  fun prt_quot {qtyp, rtyp, equiv_rel, equiv_thm} =
+    Pretty.block (Library.separate (Pretty.brk 2)
+     [Pretty.str "quotient type:",
+      Syntax.pretty_typ ctxt qtyp,
+      Pretty.str "raw type:",
+      Syntax.pretty_typ ctxt rtyp,
+      Pretty.str "relation:",
+      Syntax.pretty_term ctxt equiv_rel,
+      Pretty.str "equiv. thm:",
+      Syntax.pretty_term ctxt (prop_of equiv_thm)])
 in
   QuotData.get (ProofContext.theory_of ctxt)
   |> Symtab.dest
@@ -206,9 +206,9 @@
    val merge = Symtab.merge_list qconsts_info_eq)
 
 fun transform_qconsts phi {qconst, rconst, def} =
-    {qconst = Morphism.term phi qconst,
-     rconst = Morphism.term phi rconst,
-     def = Morphism.thm phi def}
+  {qconst = Morphism.term phi qconst,
+   rconst = Morphism.term phi rconst,
+   def = Morphism.thm phi def}
 
 fun qconsts_update_thy name qcinfo = QConstsData.map (Symtab.cons_list (name, qcinfo))
 fun qconsts_update_gen name qcinfo = Context.mapping (qconsts_update_thy name qcinfo) I
@@ -237,12 +237,12 @@
 fun print_qconstinfo ctxt =
 let
   fun prt_qconst {qconst, rconst, def} =
-      Pretty.block (separate (Pretty.brk 1)
-          [Syntax.pretty_term ctxt qconst,
-           Pretty.str ":=",
-           Syntax.pretty_term ctxt rconst,
-           Pretty.str "as",
-           Syntax.pretty_term ctxt (prop_of def)])
+    Pretty.block (separate (Pretty.brk 1)
+     [Syntax.pretty_term ctxt qconst,
+      Pretty.str ":=",
+      Syntax.pretty_term ctxt rconst,
+      Pretty.str "as",
+      Syntax.pretty_term ctxt (prop_of def)])
 in
   QConstsData.get (ProofContext.theory_of ctxt)
   |> Symtab.dest
@@ -253,9 +253,6 @@
   |> Pretty.writeln
 end
 
-(* FIXME/TODO: check the various lemmas conform *)
-(* with the required shape                      *)
-
 (* equivalence relation theorems *)
 structure EquivRules = Named_Thms
   (val name = "quot_equiv"
@@ -297,22 +294,22 @@
 (* setup of the theorem lists *)
 
 val _ = Context.>> (Context.map_theory 
-    (EquivRules.setup #>
-     RspRules.setup #>
-     PrsRules.setup #>
-     IdSimps.setup #>
-     QuotientRules.setup))
+  (EquivRules.setup #>
+   RspRules.setup #>
+   PrsRules.setup #>
+   IdSimps.setup #>
+   QuotientRules.setup))
 
 (* setup of the printing commands *)
 
-fun improper_command (pp_fn, cmd_name, descr_str) =  
-  OuterSyntax.improper_command cmd_name descr_str 
+fun improper_command (pp_fn, cmd_name, descr_str) =
+  OuterSyntax.improper_command cmd_name descr_str
     OuterKeyword.diag (Scan.succeed (Toplevel.keep (pp_fn o Toplevel.context_of)))
 
-val _ = map improper_command 
-         [(print_mapsinfo, "print_maps", "prints out all map functions"),
-          (print_quotinfo, "print_quotients", "prints out all quotients"), 
-          (print_qconstinfo, "print_quotconsts", "prints out all quotient constants")]
+val _ = map improper_command
+  [(print_mapsinfo, "print_maps", "prints out all map functions"),
+   (print_quotinfo, "print_quotients", "prints out all quotients"),
+   (print_qconstinfo, "print_quotconsts", "prints out all quotient constants")]
 
 
 end; (* structure *)