--- a/Quot/quotient_def.ML	Fri Feb 12 16:27:25 2010 +0100
+++ b/Quot/quotient_def.ML	Mon Feb 15 10:11:26 2010 +0100
@@ -20,16 +20,6 @@
 open Quotient_Info;
 open Quotient_Term;
 
-(* wrapper for define *)
-fun define name mx attr rhs lthy =
-let
-  val ((rhs, (_ , thm)), lthy') =
-     Local_Theory.define ((name, mx), (attr, rhs)) lthy
-in
-  ((rhs, thm), lthy')
-end
-
-
 (** Interface and Syntax Setup **)
 
 (* The ML-interface for a quotient definition takes
@@ -58,7 +48,7 @@
   val (_, prop') = LocalDefs.cert_def lthy prop
   val (_, newrhs) = Primitive_Defs.abs_def prop'
 
-  val ((trm, thm), lthy') = define qconst_bname mx attr newrhs lthy
+  val ((trm, (_ , thm)), lthy') = Local_Theory.define ((qconst_bname, mx), (attr, newrhs)) lthy
 
   (* data storage *)
   fun qcinfo phi = transform_qconsts phi {qconst = trm, rconst = rhs, def = thm}