# HG changeset patch
# User wenzelm
# Date 1538500204 -7200
# Node ID f33352dbbf121f67cc5728cc92cb79df434f6724
# Parent  814a1ab42d70e815013f31d2c81adb9625a3fe0c
reduce tracing messages to make it work in PIDE session;

diff -r 814a1ab42d70 -r f33352dbbf12 src/Sequents/LK/Hard_Quantifiers.thy
--- a/src/Sequents/LK/Hard_Quantifiers.thy	Tue Oct 02 19:02:47 2018 +0200
+++ b/src/Sequents/LK/Hard_Quantifiers.thy	Tue Oct 02 19:10:04 2018 +0200
@@ -248,8 +248,8 @@
 text "Problem 59"
 (*Unification works poorly here -- the abstraction %sobj prevents efficient
   operation of the occurs check*)
-
 lemma "\<turnstile> (\<forall>x. P(x) \<longleftrightarrow> \<not> P(f(x))) \<longrightarrow> (\<exists>x. P(x) \<and> \<not> P(f(x)))"
+  using [[unify_trace_bound = 50]]
   by best_dup
 
 text "Problem 60"