# HG changeset patch
# User paulson
# Date 826911664 -3600
# Node ID 3d59c407bd36b2033afe1c3957f99f833ed40f12
# Parent  bc902840aab572d066ca394a8c9d6242a4fe6826
Sets a lower value of Unify.search_bound

diff -r bc902840aab5 -r 3d59c407bd36 src/HOL/ex/MT.ML
--- a/src/HOL/ex/MT.ML	Fri Mar 15 18:39:08 1996 +0100
+++ b/src/HOL/ex/MT.ML	Fri Mar 15 18:41:04 1996 +0100
@@ -17,6 +17,10 @@
 
 open MT;
 
+(*Limit cyclic unifications during monotonicity proofs*)
+val orig_search_bound = !Unify.search_bound;
+Unify.search_bound := 8;
+
 val prems = goal MT.thy "~a:{b} ==> ~a=b";
 by (cut_facts_tac prems 1);
 by (rtac notI 1);
@@ -793,3 +797,8 @@
 by (dtac consistency 1);
 by (fast_tac (HOL_cs addSIs [basic_consistency_lem]) 1);
 qed "basic_consistency";
+
+
+Unify.search_bound := orig_search_bound;
+
+writeln"Reached end of file.";