diff -r bc02c5bfcb5b -r 0261c3eaae41 src/HOL/Modelcheck/MuckeSyn.thy
--- a/src/HOL/Modelcheck/MuckeSyn.thy	Fri Jul 24 21:34:37 2009 +0200
+++ b/src/HOL/Modelcheck/MuckeSyn.thy	Fri Jul 24 22:09:09 2009 +0200
@@ -118,7 +118,7 @@
 
 local
 
-  val move_thm = prove_goal @{theory} "[| a = b ==> P a; a = b |] ==> P b"
+  val move_thm = OldGoals.prove_goal @{theory} "[| a = b ==> P a; a = b |] ==> P b"
 	(fn prems => [cut_facts_tac prems 1, dtac sym 1, hyp_subst_tac 1,
 		     REPEAT (resolve_tac prems 1)]);
 
@@ -159,9 +159,9 @@
 
 (* transforming fun-defs into lambda-defs *)
 
-val [eq] = goal Pure.thy "(!! x. f x == g x) ==> f == g";
- by (rtac (extensional eq) 1);
-qed "ext_rl";
+val [eq] = OldGoals.goal Pure.thy "(!! x. f x == g x) ==> f == g";
+ OldGoals.by (rtac (extensional eq) 1);
+OldGoals.qed "ext_rl";
 
 infix cc;
 
@@ -196,7 +196,7 @@
 	val rhs = Syntax.string_of_term_global thy (freeze_thaw RHS)
 	val gl = delete_bold_string (fnam ^" == % " ^ (getargs LHS) ^" . " ^ rhs);
     in
-	SOME (prove_goal thy gl (fn prems =>
+	SOME (OldGoals.prove_goal thy gl (fn prems =>
   		[(REPEAT (rtac ext_rl 1)), (rtac t 1) ]))
     end
 | mk_lam_def [] _ t= NONE;