# HG changeset patch
# User wenzelm
# Date 1008365215 -3600
# Node ID 46bfc675015a0e06f9b573063ab4e096be2250c2
# Parent  5b46173df7adeb33f483ad6c69bf0518c2be6369
record: mixfix;

diff -r 5b46173df7ad -r 46bfc675015a src/HOL/thy_syntax.ML
--- 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]);