# HG changeset patch
# User Christian Urban <urbanc@in.tum.de>
# Date 1277393260 -3600
# Node ID 8a9a34be09e0407e70a0512346e9f08920a25ff1
# Parent  eadd8a4dfe78ff63f530551329cb9177492d0125
slight cleaning and simplification of the automatic wrapper for quotient definitions

diff -r eadd8a4dfe78 -r 8a9a34be09e0 src/HOL/Tools/Quotient/quotient_def.ML
--- a/src/HOL/Tools/Quotient/quotient_def.ML	Thu Jun 24 17:01:52 2010 +0200
+++ b/src/HOL/Tools/Quotient/quotient_def.ML	Thu Jun 24 16:27:40 2010 +0100
@@ -12,7 +12,7 @@
   val quotdef_cmd: (binding option * mixfix) * (Attrib.binding * (string * string)) ->
     local_theory -> Quotient_Info.qconsts_info * local_theory
 
-  val quotient_lift_const: typ list -> string * term -> local_theory ->
+  val lift_raw_const: typ list -> string * term -> local_theory ->
     Quotient_Info.qconsts_info * local_theory
 end;
 
@@ -32,12 +32,10 @@
     - the new constant as term
     - the rhs of the definition as term
 
-   It returns the defined constant and its definition
-   theorem; stores the data in the qconsts data slot.
+   It stores the qconst_info in the qconsts data slot.
 
-   Restriction: At the moment the right-hand side of the
-   definition must be a constant. Similarly the left-hand 
-   side must be a constant.
+   Restriction: At the moment the left- and right-hand 
+   side of the definition must be a constant. 
 *)
 fun error_msg bind str = 
 let 
@@ -89,10 +87,17 @@
   quotient_def (decl, (attr, (lhs, rhs))) lthy''
 end
 
-fun quotient_lift_const qtys (b, t) ctxt =
+(* a wrapper for automatically lifting a raw constant *)
+fun lift_raw_const qtys (qconst_name, rconst) ctxt =
+let
+  val rty = fastype_of rconst
+  val qty = derive_qtyp qtys rty ctxt
+in
   quotient_def ((NONE, NoSyn), (Attrib.empty_binding,
-    (Quotient_Term.quotient_lift_const qtys (b, t) ctxt, t))) ctxt
+    (Free (qconst_name, qty), rconst))) ctxt
+end
 
+(* parser and command *)
 val quotdef_decl = (Parse.binding >> SOME) -- Parse.opt_mixfix' --| Parse.$$$ "where"
 
 val quotdef_parser =
diff -r eadd8a4dfe78 -r 8a9a34be09e0 src/HOL/Tools/Quotient/quotient_term.ML
--- a/src/HOL/Tools/Quotient/quotient_term.ML	Thu Jun 24 17:01:52 2010 +0200
+++ b/src/HOL/Tools/Quotient/quotient_term.ML	Thu Jun 24 16:27:40 2010 +0100
@@ -26,7 +26,7 @@
   val inj_repabs_trm: Proof.context -> term * term -> term
   val inj_repabs_trm_chk: Proof.context -> term * term -> term
 
-  val quotient_lift_const: typ list -> string * term -> local_theory -> term
+  val derive_qtyp: typ list -> typ -> Proof.context -> typ
   val quotient_lift_all: typ list -> Proof.context -> term -> term
 end;
 
@@ -738,14 +738,12 @@
   (ty_substs, filter valid_trm_subst all_trm_substs)
 end
 
-fun quotient_lift_const qtys (b, t) ctxt =
+fun derive_qtyp qtys rty ctxt =
 let
   val thy = ProofContext.theory_of ctxt
-  val (ty_substs, _) = get_ty_trm_substs qtys ctxt;
-  val (_, ty) = dest_Const t;
-  val nty = subst_tys thy ty_substs ty;
+  val (ty_substs, _) = get_ty_trm_substs qtys ctxt
 in
-  Free(b, nty)
+  subst_tys thy ty_substs rty
 end
 
 (*