# HG changeset patch # User wenzelm # Date 1460382650 -7200 # Node ID bb3986d955621a4ea636b9b0c6df919dbe869571 # Parent 2fd4378caca2dad9cccc2fcf205e736e9eadb196 simplified constraints; diff -r 2fd4378caca2 -r bb3986d95562 src/HOL/Tools/Quotient/quotient_def.ML --- a/src/HOL/Tools/Quotient/quotient_def.ML Mon Apr 11 15:50:18 2016 +0200 +++ b/src/HOL/Tools/Quotient/quotient_def.ML Mon Apr 11 15:50:50 2016 +0200 @@ -134,16 +134,12 @@ val (opt_var, ctxt) = (case raw_var of NONE => (NONE, lthy) - | SOME var => - Proof_Context.set_object_logic_constraint lthy - |> prep_var var - ||> Proof_Context.restore_object_logic_constraint lthy - |>> SOME) - val lhs_constraint = (case opt_var of SOME (_, SOME T, _) => T | _ => dummyT) + | SOME var => prep_var var lthy |>> SOME) + val lhs_constraints = (case opt_var of SOME (_, SOME T, _) => [T] | _ => []) - fun prep_term T = parse_term ctxt #> Type.constraint T #> Syntax.check_term ctxt; - val lhs = prep_term lhs_constraint raw_lhs - val rhs = prep_term dummyT raw_rhs + fun prep_term Ts = parse_term ctxt #> fold Type.constraint Ts #> Syntax.check_term ctxt; + val lhs = prep_term lhs_constraints raw_lhs + val rhs = prep_term [] raw_rhs 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"