proper object-logic constraint (amending dd2914250ca7);

--- a/src/HOL/Tools/Quotient/quotient_def.ML	Wed Mar 30 23:34:00 2016 +0200
+++ b/src/HOL/Tools/Quotient/quotient_def.ML	Wed Mar 30 23:46:44 2016 +0200
@@ -134,7 +134,11 @@
     val (opt_var, ctxt) =
       (case raw_var of
         NONE => (NONE, lthy)
-      | SOME var => prep_var var lthy |>> SOME)
+      | 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)
 
     fun prep_term T = parse_term ctxt #> Type.constraint T #> Syntax.check_term ctxt;