--- a/src/HOL/Tools/typedef.ML Wed Feb 24 07:06:39 2010 -0800
+++ b/src/HOL/Tools/typedef.ML Wed Feb 24 20:37:01 2010 +0100
@@ -255,7 +255,7 @@
(Scan.optional (P.$$$ "(" |--
((P.$$$ "open" >> K false) -- Scan.option P.binding ||
P.binding >> (fn s => (true, SOME s))) --| P.$$$ ")") (true, NONE) --
- (P.type_args -- P.binding) -- P.opt_infix -- (P.$$$ "=" |-- P.term) --
+ (P.type_args -- P.binding) -- P.opt_mixfix -- (P.$$$ "=" |-- P.term) --
Scan.option (P.$$$ "morphisms" |-- P.!!! (P.binding -- P.binding))
>> (fn ((((((def, opt_name), (vs, t)), mx), A), morphs)) =>
Toplevel.print o Toplevel.theory_to_proof