--- a/src/HOL/Modelcheck/mucke_oracle.ML Fri Jul 24 20:55:56 2009 +0200 +++ b/src/HOL/Modelcheck/mucke_oracle.ML Fri Jul 24 21:02:34 2009 +0200 @@ -1,3 +1,4 @@ +open OldGoals; val trace_mc = ref false;