changeset 32740 | 9dd0a2f83429 |
parent 32091 | 30e2ffbba718 |
child 32960 | 69916a850301 |
--- a/src/Sequents/prover.ML Tue Sep 29 14:59:24 2009 +0200 +++ b/src/Sequents/prover.ML Tue Sep 29 16:24:36 2009 +0200 @@ -10,12 +10,11 @@ infix 4 add_safes add_unsafes; structure Cla = - struct datatype pack = Pack of thm list * thm list; -val trace = ref false; +val trace = Unsynchronized.ref false; (*A theorem pack has the form (safe rules, unsafe rules) An unsafe rule is incomplete or introduces variables in subgoals,