--- a/src/Sequents/Sequents.thy Tue Aug 07 20:19:54 2007 +0200 +++ b/src/Sequents/Sequents.thy Tue Aug 07 20:19:55 2007 +0200 @@ -11,6 +11,8 @@ uses ("prover.ML") begin +declare [[unify_trace_bound = 20, unify_search_bound = 40]] + global typedecl o