src/CTT/ex/elim.ML
changeset 18678 dd0c569fa43d
parent 15661 9ef583b08647
--- a/src/CTT/ex/elim.ML	Fri Jan 13 17:39:41 2006 +0100
+++ b/src/CTT/ex/elim.ML	Sat Jan 14 17:14:06 2006 +0100
@@ -20,7 +20,7 @@
 result();
 writeln"first solution is fst;  backtracking gives snd";
 back(); 
-back() handle ERROR => writeln"And there are indeed no others";  
+back() handle ERROR _ => writeln"And there are indeed no others";  
 
 
 writeln"Double negation of the Excluded Middle";