src/HOL/Tools/Quotient/quotient_def.ML

--- a/src/HOL/Tools/Quotient/quotient_def.ML	Thu Apr 05 16:25:59 2012 +0200
+++ b/src/HOL/Tools/Quotient/quotient_def.ML	Thu Apr 05 22:00:27 2012 +0200
@@ -18,7 +18,7 @@
     (binding * string option * mixfix) option * (Attrib.binding * (string * string)) ->
     local_theory -> Proof.state
 
-  val lift_raw_const: typ list -> (string * term * mixfix) -> local_theory ->
+  val lift_raw_const: typ list -> (string * term * mixfix) -> thm -> local_theory ->
     Quotient_Info.quotconsts * local_theory
 end;
 
@@ -332,14 +332,24 @@
 
 
 (* a wrapper for automatically lifting a raw constant *)
-fun lift_raw_const qtys (qconst_name, rconst, mx) ctxt =
+fun lift_raw_const qtys (qconst_name, rconst, mx') rsp_thm lthy =
   let
     val rty = fastype_of rconst
-    val qty = Quotient_Term.derive_qtyp ctxt qtys rty
-    val lhs = Free (qconst_name, qty)
+    val qty = Quotient_Term.derive_qtyp lthy qtys rty
+    val lhs_raw = Free (qconst_name, qty)
+    val rhs_raw = rconst
+
+    val raw_var = (Binding.name qconst_name, NONE, mx')
+    val ([(binding, _, mx)], ctxt) = Proof_Context.cert_vars [raw_var] lthy
+    val lhs = Syntax.check_term ctxt lhs_raw
+    val rhs = Syntax.check_term ctxt rhs_raw
+
+    val (lhs_str, lhs_ty) = dest_Free lhs handle TERM _ => error "Constant already defined."
+    val _ = if null (strip_abs_vars rhs) then () else error "The definiens cannot be an abstraction"
+    val _ = if is_Const rhs then () else warning "The definiens is not a constant"
+
   in
-    (*quotient_def (SOME (Binding.name qconst_name, NONE, mx), (Attrib.empty_binding, (lhs, rconst))) ctxt*)
-    ({qconst = lhs, rconst = lhs, def = @{thm refl}}, ctxt)
+    add_quotient_def (((binding, mx), Attrib.empty_binding), (lhs, rhs)) rsp_thm  ctxt
   end
 
 (* parser and command *)