record: mixfix;

--- a/src/HOL/thy_syntax.ML	Fri Dec 14 11:57:03 2001 +0100
+++ b/src/HOL/thy_syntax.ML	Fri Dec 14 22:26:55 2001 +0100
@@ -34,7 +34,7 @@
 val record_decl =
   (type_args -- name >> (mk_pair o apfst mk_list)) --$$ "="
     -- optional (typ --$$ "+" >> (parens o cat "Some")) "None"
-    -- repeat1 ((name --$$ "::" -- typ) >> mk_pair)
+    -- repeat1 ((name --$$ "::" -- !! (typ -- opt_mixfix)) >> mk_triple2)
   >> (fn ((x, y), zs) => cat_lines [x, y, mk_big_list zs]);