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