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