--- a/src/HOL/Hoare/List_Examples.ML	Mon Jun 22 17:13:09 1998 +0200
+++ b/src/HOL/Hoare/List_Examples.ML	Mon Jun 22 17:26:46 1998 +0200
@@ -1,4 +1,4 @@
-goal thy
+Goal
 "{x=X} \
 \ y := []; \
 \ WHILE x ~= [] \
@@ -12,7 +12,7 @@
 by (Asm_full_simp_tac 1);
 qed "imperative_reverse";
 
-goal thy
+Goal
 "{x=X & y = Y} \
 \ x := rev(x); \
 \ WHILE x ~= [] \