# HG changeset patch
# User paulson
# Date 878385631 -3600
# Node ID 5a2cc5752cb660e362b50b2c1923b9a3b012335b
# Parent  600f266eac454e82daf0f347ec61c8c1bffe5070
mended type constraint\!

diff -r 600f266eac45 -r 5a2cc5752cb6 src/HOL/ex/cla.ML
--- a/src/HOL/ex/cla.ML	Sat Nov 01 13:00:03 1997 +0100
+++ b/src/HOL/ex/cla.ML	Sat Nov 01 13:00:31 1997 +0100
@@ -89,7 +89,7 @@
 result();
 
 (*11.  Proved in each direction (incorrectly, says Pelletier!!)  *)
-goal HOL.thy "P=P::bool";
+goal HOL.thy "P=(P::bool)";
 by (Blast_tac 1);
 result();