diff -r 0fd4abb5fade -r f51c6069cd17 Quot/quotient_def.ML
--- a/Quot/quotient_def.ML	Fri Dec 11 08:28:41 2009 +0100
+++ b/Quot/quotient_def.ML	Fri Dec 11 11:08:58 2009 +0100
@@ -3,12 +3,9 @@
 sig
   datatype flag = absF | repF
   val get_fun: flag -> Proof.context -> typ * typ -> term
-  val make_def: binding -> mixfix -> Attrib.binding -> term -> term ->
+  val make_def: mixfix -> Attrib.binding -> term -> term ->
     Proof.context -> (term * thm) * local_theory
-
-  val quotdef: (binding * term * mixfix) * (Attrib.binding * term) ->
-    local_theory -> (term * thm) * local_theory
-  val quotdef_cmd: (binding * string * mixfix) * (Attrib.binding * string) ->
+  val quotdef_cmd: (Attrib.binding * string) * (mixfix * string) ->
     local_theory -> local_theory
 end;
 
@@ -79,9 +76,11 @@
   | (TVar _, TVar _) => raise (LIFT_MATCH "get_fun")
   | _ => raise (LIFT_MATCH "get_fun")
 
-fun make_def qconst_bname mx attr lhs rhs lthy =
+fun make_def mx attr lhs rhs lthy =
 let
-  val absrep_trm = get_fun absF lthy (fastype_of rhs, fastype_of lhs) $ rhs
+  val Free (lhs_str, lhs_ty) = lhs;
+  val qconst_bname = Binding.name lhs_str;
+  val absrep_trm = get_fun absF lthy (fastype_of rhs, lhs_ty) $ rhs
                    |> Syntax.check_term lthy
   val prop = Logic.mk_equals (lhs, absrep_trm)
   val (_, prop') = LocalDefs.cert_def lthy prop
@@ -91,12 +90,7 @@
 
   fun qcinfo phi = qconsts_transfer phi {qconst = trm, rconst = rhs, def = thm}
   val lthy'' = Local_Theory.declaration true
-                 (fn phi => 
-                       let
-                         val qconst_str = Binding.name_of qconst_bname
-                       in                      
-                         qconsts_update_gen qconst_str (qcinfo phi)
-                       end) lthy'
+                 (fn phi => qconsts_update_gen lhs_str (qcinfo phi)) lthy'
 in
   ((trm, thm), lthy'')
 end
@@ -111,22 +105,21 @@
 (* - a meta-equation defining the constant,        *)
 (*   and the attributes of for this meta-equality  *)
 
-fun quotdef ((bind, lhs, mx), (attr, rhs)) lthy =
-  make_def bind mx attr lhs rhs lthy
-
-fun quotdef_cmd ((bind, lhsstr, mx), (attr, 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
-  quotdef ((bind, lhs, mx), (attr, rhs)) lthy |> snd
+  make_def mx attr lhs rhs lthy |> snd
 end
 
+val _ = OuterKeyword.keyword "as";
+
 val quotdef_parser =
-  (OuterParse.binding --
-    (OuterParse.$$$ "::" |-- OuterParse.!!! (OuterParse.term --
-      OuterParse.opt_mixfix' --| OuterParse.where_)) >> OuterParse.triple2) --
-       (SpecParse.opt_thm_name ":" -- OuterParse.term)
+  (SpecParse.opt_thm_name ":" --
+  OuterParse.term) --
+  (OuterParse.opt_mixfix' --| OuterParse.$$$ "as" --
+  OuterParse.term)
 
 val _ = OuterSyntax.local_theory "quotient_def" "lifted definition of constants"
   OuterKeyword.thy_decl (quotdef_parser >> quotdef_cmd)