# HG changeset patch
# User wenzelm
# Date 1459374404 -7200
# Node ID b486f512a471aaf44c05699affd0ab636ad5ccdb
# Parent  cfcb20bbdbd8bd2934e3a07afde0e681c1e8173d
proper object-logic constraint (amending dd2914250ca7);

diff -r cfcb20bbdbd8 -r b486f512a471 src/HOL/Tools/Quotient/quotient_def.ML
--- 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;