--- a/quotient.ML	Thu Nov 05 10:46:54 2009 +0100
+++ b/quotient.ML	Thu Nov 05 13:47:04 2009 +0100
@@ -1,7 +1,7 @@
 signature QUOTIENT =
 sig
-  val mk_quotient_type: ((binding * mixfix) * (typ * term)) list -> Proof.context -> Proof.state
-  val mk_quotient_type_cmd: (((bstring * mixfix) * string) * string) list -> Proof.context -> Proof.state
+  val quotient_type: ((binding * mixfix) * (typ * term)) list -> Proof.context -> Proof.state
+  val quotient_type_cmd: (((bstring * mixfix) * string) * string) list -> Proof.context -> Proof.state
   val define: binding * mixfix * term -> local_theory -> (term * thm) * local_theory
   val note: binding * thm -> local_theory -> thm * local_theory
 end;
@@ -190,7 +190,7 @@
 (* - the type to be quotient                                *)
 (* - the relation according to which the type is quotient   *)
 
-fun mk_quotient_type quot_list lthy = 
+fun quotient_type quot_list lthy = 
 let
   fun mk_goal (rty, rel) =
   let
@@ -207,7 +207,7 @@
   theorem after_qed goals lthy
 end
            
-fun mk_quotient_type_cmd spec lthy = 
+fun quotient_type_cmd spec lthy = 
 let
   fun parse_spec (((qty_str, mx), rty_str), rel_str) =
   let
@@ -218,7 +218,7 @@
     ((qty_name, mx), (rty, rel))
   end
 in
-  mk_quotient_type (map parse_spec spec) lthy
+  quotient_type (map parse_spec spec) lthy
 end
 
 val quotspec_parser = 
@@ -232,7 +232,7 @@
 val _ = 
     OuterSyntax.local_theory_to_proof "quotient" 
       "quotient type definitions (requires equivalence proofs)"
-         OuterKeyword.thy_goal (quotspec_parser >> mk_quotient_type_cmd)
+         OuterKeyword.thy_goal (quotspec_parser >> quotient_type_cmd)
 
 end; (* structure *)