src/FOLP/ex/foundn.ML
changeset 18678 dd0c569fa43d
parent 17480 fd19f77dcf60
--- a/src/FOLP/ex/foundn.ML	Fri Jan 13 17:39:41 2006 +0100
+++ b/src/FOLP/ex/foundn.ML	Sat Jan 14 17:14:06 2006 +0100
@@ -92,7 +92,7 @@
 goal (theory "IFOLP") "?p : EX y. ALL x. x=y";
 by (rtac exI 1);
 by (rtac allI 1);
-by (rtac refl 1) handle ERROR => writeln"Failed, as expected";  
+by (rtac refl 1) handle ERROR _ => writeln"Failed, as expected";  
 getgoal 1;