diff -r 5a50de9141b5 -r fe09a0c5cebe src/HOL/Modelcheck/MuckeExample1.ML
--- a/src/HOL/Modelcheck/MuckeExample1.ML	Thu Aug 19 19:01:57 1999 +0200
+++ b/src/HOL/Modelcheck/MuckeExample1.ML	Thu Aug 19 19:55:13 1999 +0200
@@ -6,16 +6,12 @@
 
 val reach_rws = [INIT_def,N_def,reach_def];
 
-(*
-goal thy "reach (True,True,True)";
+Goal "reach (True,True,True)";
 by (simp_tac (Mucke_ss addsimps reach_rws) 1); 
-by (mc_mucke_tac thy [] 1);
+by (mc_mucke_tac [] 1);
 qed "reach_ex_thm1";
 
-(* Alternative: *)
-goal thy "reach (True,True,True)";
-by (mc_mucke_tac thy reach_rws 1);
-qed "reach_ex_thm1";
-
-*)
-
+(*alternative*)
+Goal "reach (True,True,True)";
+by (mc_mucke_tac reach_rws 1);
+qed "reach_ex_thm1'";