--- a/src/HOL/Integ/IntRingDefs.ML	Mon Jun 22 17:13:09 1998 +0200
+++ b/src/HOL/Integ/IntRingDefs.ML	Mon Jun 22 17:26:46 1998 +0200
@@ -7,10 +7,10 @@
 
 open IntRingDefs;
 
-goalw thy [zero_int_def,zdiff_def] "(zero-x)+(x::int) = zero";
+Goalw [zero_int_def,zdiff_def] "(zero-x)+(x::int) = zero";
 by (Simp_tac 1);
 qed "left_inv_int";
 
-goalw thy [zero_int_def,zdiff_def] "x-y = (x::int) + (zero-y)";
+Goalw [zero_int_def,zdiff_def] "x-y = (x::int) + (zero-y)";
 by (Simp_tac 1);
 qed "minus_inv_int";