diff -r 243a5ceaa088 -r 17ca92ab4660 Quot/quotient_def.ML
--- a/Quot/quotient_def.ML	Thu Feb 11 09:23:59 2010 +0100
+++ b/Quot/quotient_def.ML	Thu Feb 11 10:06:02 2010 +0100
@@ -6,7 +6,7 @@
 *)
 
 signature QUOTIENT_DEF =
-sig 
+sig
   val quotient_def: mixfix -> Attrib.binding -> term -> term ->
     local_theory -> (term * thm) * local_theory
 
@@ -32,7 +32,7 @@
 
 (** Interface and Syntax Setup **)
 
-(* The ML-interface for a quotient definition takes 
+(* The ML-interface for a quotient definition takes
    as argument:
 
     - the mixfix annotation
@@ -41,11 +41,11 @@
     - the rhs of the definition as term
 
    It returns the defined constant and its definition
-   theorem; stores the data in the qconsts data slot. 
+   theorem; stores the data in the qconsts data slot.
 
    Restriction: At the moment the right-hand side must
-   be a terms composed of constant. Similarly the 
-   left-hand side must be a single constant.   
+   be a terms composed of constant. Similarly the
+   left-hand side must be a single constant.
 *)
 fun quotient_def mx attr lhs rhs lthy =
 let
@@ -87,7 +87,7 @@
       (OuterParse.opt_mixfix' --| OuterParse.$$$ "as" --
          OuterParse.term)
 
-val _ = OuterSyntax.local_theory "quotient_definition" 
+val _ = OuterSyntax.local_theory "quotient_definition"
 	  "definition for constants over the quotient type"
              OuterKeyword.thy_decl (quotdef_parser >> quotdef_cmd)