src/FOLP/ex/foundn.ML

 
 
 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; 
 
 
 (*Parallel lifting example. *)
 goal (theory "IFOLP") "?p : EX u. ALL x. EX v. ALL y. EX w. P(u,x,v,y,w)";