diff -r 6f6ee78c7357 -r ba7e81531c6d Quot/quotient_def.ML
--- a/Quot/quotient_def.ML	Fri Jan 01 11:30:00 2010 +0100
+++ b/Quot/quotient_def.ML	Fri Jan 01 23:59:32 2010 +0100
@@ -26,15 +26,15 @@
 
 (* interface and syntax setup *)
 
-(* the ML-interface takes a 4-tuple consisting of  *)
-(*                                                 *)
-(* - the mixfix annotation                         *)
-(* - name and attributes                           *)
-(* - the new constant including its type           *)
-(* - the rhs of the definition                     *)
-(*                                                 *)
-(* returns the defined constant and its definition *)
-(* theorem; stores the data in the qconsts slot    *)
+(* the ML-interface takes a 4-tuple consisting of     *)
+(*                                                    *)
+(* - 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       *)
 
 fun quotient_def mx attr lhs rhs lthy =
 let
@@ -55,10 +55,10 @@
   ((trm, thm), lthy'')
 end
 
-fun quotdef_cmd ((attr, lhsstr), (mx, rhsstr)) lthy =
+fun quotdef_cmd ((attr, lhs_str), (mx, rhs_str)) lthy =
 let
-  val lhs = Syntax.read_term lthy lhsstr
-  val rhs = Syntax.read_term lthy rhsstr
+  val lhs = Syntax.read_term lthy lhs_str
+  val rhs = Syntax.read_term lthy rhs_str
 in
   quotient_def mx attr lhs rhs lthy |> snd
 end