--- 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"