diff -r 0ce025c02ef3 -r bb012513fb39 Quot/quotient_def.ML
--- a/Quot/quotient_def.ML	Wed Jan 13 09:30:59 2010 +0100
+++ b/Quot/quotient_def.ML	Wed Jan 13 09:41:57 2010 +0100
@@ -28,14 +28,14 @@
 
 (* the ML-interface takes
 
- - the mixfix annotation
- - name and attributes
- - the new constant as term
- - the rhs of the definition as term
+  - the mixfix annotation
+  - name and attributes
+  - the new constant as term
+  - the rhs of the definition as term
 
- it returns the defined constant and its definition
- theorem; stores the data in the qconsts slot       *)
-
+  it returns the defined constant and its definition
+  theorem; stores the data in the qconsts slot       
+*)
 fun quotient_def mx attr lhs rhs lthy =
 let
   val Free (lhs_str, lhs_ty) = lhs; (* FIXME/TODO: this throws an excpt., if the const is already def.*)