src/HOL/ex/Puzzle.ML

--- a/src/HOL/ex/Puzzle.ML	Wed Oct 07 10:30:47 1998 +0200
+++ b/src/HOL/ex/Puzzle.ML	Wed Oct 07 10:31:07 1998 +0200
@@ -51,7 +51,7 @@
 qed "mono_lemma";
 
 val prems = goal Puzzle.thy "m <= n ==> f(m) <= f(n)";
-by (fast_tac (claset() addIs ([mono_lemma,less_imp_le,lemma2]@prems)) 1);
+by (fast_tac (claset() addIs [mono_lemma,less_imp_le,lemma2]@prems) 1);
 qed "f_mono";
 
 Goal "f(n) = n";