--- 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));