# HG changeset patch
# User Cezary Kaliszyk <kaliszyk@in.tum.de>
# Date 1266488356 -3600
# Node ID e5413596e0988ba2511fb5972ab9d8eaa7c2c62f
# Parent  3b24f33aedad5718703226e858a04b05b91322a9
Automatic lifting of constants.

diff -r 3b24f33aedad -r e5413596e098 Quot/quotient_def.ML
--- a/Quot/quotient_def.ML	Thu Feb 18 10:01:48 2010 +0100
+++ b/Quot/quotient_def.ML	Thu Feb 18 11:19:16 2010 +0100
@@ -12,6 +12,8 @@
 
   val quotdef_cmd: (binding option * mixfix) * (Attrib.binding * (string * string)) ->
     local_theory -> (term * thm) * local_theory
+
+  val quotient_lift_const: string * term -> local_theory -> (term * thm) * local_theory
 end;
 
 structure Quotient_Def: QUOTIENT_DEF =
@@ -85,6 +87,10 @@
   quotient_def (decl, (attr, (lhs, rhs))) lthy''
 end
 
+fun quotient_lift_const (b, t) ctxt =
+  quotient_def ((NONE, NoSyn), (Attrib.empty_binding,
+    (Quotient_Term.quotient_lift_const (b, t) ctxt, t))) ctxt
+
 local
   structure P = OuterParse;
 in
diff -r 3b24f33aedad -r e5413596e098 Quot/quotient_term.ML
--- a/Quot/quotient_term.ML	Thu Feb 18 10:01:48 2010 +0100
+++ b/Quot/quotient_term.ML	Thu Feb 18 11:19:16 2010 +0100
@@ -26,6 +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: string * term -> local_theory -> term
   val quotient_lift_all: Proof.context -> term -> term
 end;
 
@@ -732,6 +733,15 @@
   (ty_substs, const_substs @ rel_substs)
 end
 
+fun quotient_lift_const (b, t) ctxt =
+let
+  val thy = ProofContext.theory_of ctxt
+  val (ty_substs, _) = get_ty_trm_substs ctxt;
+  val (_, ty) = dest_Const t;
+  val nty = subst_tys thy ty_substs ty;
+in
+  Free(b, nty)
+end
 
 (*
 Takes a term and