--- a/Quot/quotient_def.ML	Wed Dec 09 06:21:09 2009 +0100
+++ b/Quot/quotient_def.ML	Wed Dec 09 15:57:47 2009 +0100
@@ -3,10 +3,10 @@
 sig
   datatype flag = absF | repF
   val get_fun: flag -> Proof.context -> typ * typ -> term
-  val make_def: binding -> typ -> mixfix -> Attrib.binding -> term ->
+  val make_def: binding -> mixfix -> Attrib.binding -> term -> term ->
     Proof.context -> (term * thm) * local_theory
 
-  val quotdef: (binding * typ * mixfix) * (Attrib.binding * term) ->
+  val quotdef: (binding * term * mixfix) * (Attrib.binding * term) ->
     local_theory -> (term * thm) * local_theory
   val quotdef_cmd: (binding * string * mixfix) * (Attrib.binding * string) ->
     local_theory -> local_theory
@@ -79,18 +79,22 @@
   | (TVar _, TVar _) => raise (LIFT_MATCH "get_fun")
   | _ => raise (LIFT_MATCH "get_fun")
 
-fun make_def qconst_bname qty mx attr rhs lthy =
+fun make_def qconst_bname mx attr lhs rhs lthy =
 let
-  val absrep_trm = get_fun absF lthy (fastype_of rhs, qty) $ rhs
-                   |> Syntax.check_term lthy 
+  val absrep_trm = get_fun absF lthy (fastype_of rhs, fastype_of lhs) $ rhs
+                   |> Syntax.check_term lthy
+  val prop = Logic.mk_equals (lhs, absrep_trm)
+  val (_, prop') = LocalDefs.cert_def lthy prop
+  val (_, newrhs) = Primitive_Defs.abs_def prop'
 
-  val ((trm, thm), lthy') = define qconst_bname mx attr absrep_trm lthy
+  val ((trm, thm), lthy') = define qconst_bname mx attr newrhs lthy
 
   fun qcinfo phi = qconsts_transfer phi {qconst = trm, rconst = rhs, def = thm}
   val lthy'' = Local_Theory.declaration true
+   val lthy'' = Local_Theory.declaration true
                  (fn phi => 
                        let
-                         val qconst_str = fst (Term.dest_Const (Morphism.term phi trm))
+                         val qconst_str = Binding.name_of qconst_bname
                        in                      
                          qconsts_update_gen qconst_str (qcinfo phi)
                        end) lthy'
@@ -108,27 +112,22 @@
 (* - a meta-equation defining the constant,        *)
 (*   and the attributes of for this meta-equality  *)
 
-fun quotdef ((bind, qty, mx), (attr, prop)) lthy =
-let   
-  val (_, prop') = LocalDefs.cert_def lthy prop
-  val (_, rhs) = Primitive_Defs.abs_def prop'
-in  
-  make_def bind qty mx attr rhs lthy 
-end
+fun quotdef ((bind, lhs, mx), (attr, rhs)) lthy =
+  make_def bind mx attr lhs rhs lthy
 
-fun quotdef_cmd ((bind, qtystr, mx), (attr, propstr)) lthy = 
+fun quotdef_cmd ((bind, lhsstr, mx), (attr, rhsstr)) lthy = 
 let
-  val qty  = Syntax.read_typ lthy qtystr
-  val prop = Syntax.read_prop lthy propstr
+  val lhs = Syntax.read_term lthy lhsstr
+  val rhs = Syntax.read_term lthy rhsstr
 in
-  quotdef ((bind, qty, mx), (attr, prop)) lthy |> snd
+  quotdef ((bind, lhs, mx), (attr, rhs)) lthy |> snd
 end
 
 val quotdef_parser =
   (OuterParse.binding --
-    (OuterParse.$$$ "::" |-- OuterParse.!!! (OuterParse.typ -- 
-      OuterParse.opt_mixfix' --| OuterParse.where_)) >> OuterParse.triple2) -- 
-       (SpecParse.opt_thm_name ":" -- OuterParse.prop)
+    (OuterParse.$$$ "::" |-- OuterParse.!!! (OuterParse.term --
+      OuterParse.opt_mixfix' --| OuterParse.where_)) >> OuterParse.triple2) --
+       (SpecParse.opt_thm_name ":" -- OuterParse.term)
 
 val _ = OuterSyntax.local_theory "quotient_def" "lifted definition of constants"
   OuterKeyword.thy_decl (quotdef_parser >> quotdef_cmd)