1.1 --- a/src/HOL/Tools/Quotient/quotient_def.ML	Mon Jul 04 22:25:33 2011 +0200
     1.2 +++ b/src/HOL/Tools/Quotient/quotient_def.ML	Tue Jul 05 09:54:39 2011 +0200
     1.3 @@ -46,8 +46,9 @@
     1.4  fun gen_quotient_def prep_vars prep_term (raw_var, (attr, (lhs_raw, rhs_raw))) lthy =
     1.5    let
     1.6      val (vars, ctxt) = prep_vars (the_list raw_var) lthy
     1.7 -    val lhs = prep_term ctxt lhs_raw
     1.8 -    val rhs = prep_term ctxt rhs_raw
     1.9 +    val T_opt = (case vars of [(_, SOME T, _)] => SOME T | _ => NONE)
    1.10 +    val lhs = prep_term T_opt ctxt lhs_raw
    1.11 +    val rhs = prep_term NONE ctxt rhs_raw
    1.12  
    1.13      val (lhs_str, lhs_ty) = dest_Free lhs handle TERM _ => error "Constant already defined."
    1.14      val _ = if null (strip_abs_vars rhs) then () else error "The definiens cannot be an abstraction"
    1.15 @@ -80,8 +81,12 @@
    1.16      (qconst_data, lthy'')
    1.17    end
    1.18  
    1.19 -val quotient_def = gen_quotient_def Proof_Context.cert_vars Syntax.check_term
    1.20 -val quotdef_cmd = gen_quotient_def Proof_Context.read_vars Syntax.read_term
    1.21 +fun check_term' cnstr ctxt =
    1.22 +  Syntax.check_term ctxt o (case cnstr of SOME T => Type.constraint T | _ => I)
    1.23 +fun read_term' cnstr ctxt = check_term' cnstr ctxt o tap (writeln o @{make_string}) o Syntax.parse_term ctxt
    1.24 +
    1.25 +val quotient_def = gen_quotient_def Proof_Context.cert_vars check_term'
    1.26 +val quotdef_cmd = gen_quotient_def Proof_Context.read_vars read_term'
    1.27  
    1.28  
    1.29  (* a wrapper for automatically lifting a raw constant *)