diff -r bd13a0017137 -r 3ba9eb7ea366 src/HOL/Tools/typedef_package.ML
--- a/src/HOL/Tools/typedef_package.ML	Tue May 31 11:53:16 2005 +0200
+++ b/src/HOL/Tools/typedef_package.ML	Tue May 31 11:53:17 2005 +0200
@@ -375,9 +375,9 @@
 
 
 val typedef_proof_decl =
-  Scan.optional (P.$$$ "(" |-- P.!!!
-      (((P.$$$ "open" >> K false) -- Scan.option P.name || P.name >> (fn s => (true, SOME s)))
-        --| P.$$$ ")")) (true, NONE) --
+  Scan.optional (P.$$$ "(" |--
+      ((P.$$$ "open" >> K false) -- Scan.option P.name || P.name >> (fn s => (true, SOME s)))
+        --| P.$$$ ")") (true, NONE) --
     (P.type_args -- P.name) -- P.opt_infix -- (P.$$$ "=" |-- P.term) --
     Scan.option (P.$$$ "morphisms" |-- P.!!! (P.name -- P.name));