--- a/src/HOL/Modelcheck/MuckeExample2.ML	Thu Aug 19 19:01:57 1999 +0200
+++ b/src/HOL/Modelcheck/MuckeExample2.ML	Thu Aug 19 19:55:13 1999 +0200
@@ -9,20 +9,12 @@
 (* trace_mc := true; *)
 val Reach_rws = [Init_def,R_def,Reach_def,Reach2_def];
 
-(*
-
-goal thy "Reach2 True";
+Goal "Reach2 True";
 by (simp_tac (Mucke_ss addsimps Reach_rws) 1);
-by (mc_mucke_tac thy [] 1);
+by (mc_mucke_tac [] 1);
 qed "Reach_thm";
 
-(* Alternative: *)
+(*alternative:*)
 goal thy "Reach2 True";
-by (mc_mucke_tac thy Reach_rws 1);
-qed "Reach_thm";
-
-
-*)
-
-
-  
+by (mc_mucke_tac Reach_rws 1);
+qed "Reach_thm'";