diff -r f51c6069cd17 -r 596467882518 Quot/quotient_def.ML
--- a/Quot/quotient_def.ML	Fri Dec 11 11:08:58 2009 +0100
+++ b/Quot/quotient_def.ML	Fri Dec 11 11:19:41 2009 +0100
@@ -3,7 +3,7 @@
 sig
   datatype flag = absF | repF
   val get_fun: flag -> Proof.context -> typ * typ -> term
-  val make_def: mixfix -> Attrib.binding -> term -> term ->
+  val quotient_def: mixfix -> Attrib.binding -> term -> term ->
     Proof.context -> (term * thm) * local_theory
   val quotdef_cmd: (Attrib.binding * string) * (mixfix * string) ->
     local_theory -> local_theory
@@ -76,7 +76,15 @@
   | (TVar _, TVar _) => raise (LIFT_MATCH "get_fun")
   | _ => raise (LIFT_MATCH "get_fun")
 
-fun make_def mx attr lhs rhs lthy =
+(* interface and syntax setup *)
+
+(* the ML-interface takes a 4-tuple consisting of *)
+(*                                                *)
+(* - the mixfix annotation                        *)
+(* - name and attributes of the meta eq           *)
+(* - the new constant including its type          *)
+(* - the rhs of the definition                    *)
+fun quotient_def mx attr lhs rhs lthy =
 let
   val Free (lhs_str, lhs_ty) = lhs;
   val qconst_bname = Binding.name lhs_str;
@@ -95,22 +103,12 @@
   ((trm, thm), lthy'')
 end
 
-(* interface and syntax setup *)
-
-(* the ML-interface takes a 5-tuple consisting of  *)
-(*                                                 *)
-(* - the name of the constant to be lifted         *)
-(* - its type                                      *)
-(* - its mixfix annotation                         *)
-(* - a meta-equation defining the constant,        *)
-(*   and the attributes of for this meta-equality  *)
-
-fun quotdef_cmd ((attr, lhsstr), (mx, rhsstr)) lthy = 
+fun quotdef_cmd ((attr, lhsstr), (mx, rhsstr)) lthy =
 let
   val lhs = Syntax.read_term lthy lhsstr
   val rhs = Syntax.read_term lthy rhsstr
 in
-  make_def mx attr lhs rhs lthy |> snd
+  quotient_def mx attr lhs rhs lthy |> snd
 end
 
 val _ = OuterKeyword.keyword "as";