--- 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 *)