| changeset 32740 | 9dd0a2f83429 |
| parent 32178 | 0261c3eaae41 |
| child 32960 | 69916a850301 |
--- a/src/HOL/Modelcheck/mucke_oracle.ML Tue Sep 29 14:59:24 2009 +0200 +++ b/src/HOL/Modelcheck/mucke_oracle.ML Tue Sep 29 16:24:36 2009 +0200 @@ -1,5 +1,5 @@ -val trace_mc = ref false; +val trace_mc = Unsynchronized.ref false; (* transform_case post-processes output strings of the syntax "Mucke" *)