# HG changeset patch
# User krauss
# Date 1309852479 -7200
# Node ID e8c80bbc0c5d6f4b555273b625e1de3d11358c95
# Parent  e3175ec00311f6c9788348aee636598f3c0d1230
re-check to explicitly propagate a given type constraint to lhs -- necessary to trigger type improvement in an instantiation target

diff -r e3175ec00311 -r e8c80bbc0c5d src/HOL/Tools/Quotient/quotient_def.ML
--- a/src/HOL/Tools/Quotient/quotient_def.ML	Mon Jul 04 22:25:33 2011 +0200
+++ b/src/HOL/Tools/Quotient/quotient_def.ML	Tue Jul 05 09:54:39 2011 +0200
@@ -46,8 +46,9 @@
 fun gen_quotient_def prep_vars prep_term (raw_var, (attr, (lhs_raw, rhs_raw))) lthy =
   let
     val (vars, ctxt) = prep_vars (the_list raw_var) lthy
-    val lhs = prep_term ctxt lhs_raw
-    val rhs = prep_term ctxt rhs_raw
+    val T_opt = (case vars of [(_, SOME T, _)] => SOME T | _ => NONE)
+    val lhs = prep_term T_opt ctxt lhs_raw
+    val rhs = prep_term NONE 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"
@@ -80,8 +81,12 @@
     (qconst_data, lthy'')
   end
 
-val quotient_def = gen_quotient_def Proof_Context.cert_vars Syntax.check_term
-val quotdef_cmd = gen_quotient_def Proof_Context.read_vars Syntax.read_term
+fun check_term' cnstr ctxt =
+  Syntax.check_term ctxt o (case cnstr of SOME T => Type.constraint T | _ => I)
+fun read_term' cnstr ctxt = check_term' cnstr ctxt o tap (writeln o @{make_string}) o Syntax.parse_term ctxt
+
+val quotient_def = gen_quotient_def Proof_Context.cert_vars check_term'
+val quotdef_cmd = gen_quotient_def Proof_Context.read_vars read_term'
 
 
 (* a wrapper for automatically lifting a raw constant *)