src/CTT/ex/elim.ML

--- a/src/CTT/ex/elim.ML	Fri Oct 10 16:29:41 1997 +0200
+++ b/src/CTT/ex/elim.ML	Fri Oct 10 17:10:12 1997 +0200
@@ -148,7 +148,7 @@
 
 writeln"Axiom of choice.  Proof without fst, snd.  Harder still!"; 
 val prems = goal CTT.thy   
-    "[| A type;  !!x.x:A ==> B(x) type;                         \
+    "[| A type;  !!x. x:A ==> B(x) type;                         \
 \       !!x y.[| x:A;  y:B(x) |] ==> C(x,y) type                \
 \    |] ==> ?a : PROD h: (PROD x:A. SUM y:B(x). C(x,y)).        \
 \                        (SUM f: (PROD x:A. B(x)). PROD x:A. C(x, f`x))";