1.1 --- a/src/Pure/Thy/thy_parse.ML	Fri Dec 01 13:41:48 1995 +0100
     1.2 +++ b/src/Pure/Thy/thy_parse.ML	Fri Dec 01 13:54:27 1995 +0100
     1.3 @@ -230,35 +230,6 @@
     1.4  
     1.5  (* types *)
     1.6  
     1.7 -fun mk_old_type_decl ((ts, n), syn) =
     1.8 -  map (fn t => (mk_triple (t, n, syn), false)) ts;
     1.9 -
    1.10 -fun mk_type_decl (((xs, t), None), syn) =
    1.11 -      [(mk_triple (t, string_of_int (length xs), syn), false)]
    1.12 -  | mk_type_decl (((xs, t), Some rhs), syn) =
    1.13 -      [(parens (commas [t, mk_list xs, rhs, syn]), true)];
    1.14 -
    1.15 -fun mk_type_decls tys =
    1.16 -  "|> add_types\n" ^ mk_big_list (keyfilter tys false) ^ "\n\n\
    1.17 -  \|> add_tyabbrs\n" ^ mk_big_list (keyfilter tys true);
    1.18 -
    1.19 -
    1.20 -val old_type_decl = names1 -- nat -- opt_infix >> mk_old_type_decl;
    1.21 -
    1.22 -val type_args =
    1.23 -  type_var >> (fn x => [x]) ||
    1.24 -  "(" $$-- !! (list1 type_var --$$ ")") ||
    1.25 -  empty >> K [];
    1.26 -
    1.27 -val type_decl = type_args -- name -- optional ("=" $$-- !! string >> Some) None
    1.28 -  -- opt_infix >> mk_type_decl;
    1.29 -
    1.30 -val type_decls = repeat1 (old_type_decl || type_decl) >>
    1.31 -                 (mk_type_decls o flat);
    1.32 -
    1.33 -
    1.34 -(* consts *)
    1.35 -
    1.36  (*Parse an identifier, but only if it is not followed by colons or a comma;
    1.37    the exclusion of a postfix comma can be controlled to allow expressions
    1.38    like "(id, id)" but disallow ones like "'a => id id,id :: ..."*)
    1.39 @@ -272,6 +243,7 @@
    1.40    | ident_no_colon _ ((k, s, n) :: _) =
    1.41        syn_err (name_of_kind Ident) (quote s) n;
    1.42  
    1.43 +(*Type used in types, consts and syntax sections*)
    1.44  fun const_type allow_comma toks =
    1.45    let val simple_type =
    1.46          (ident ||
    1.47 @@ -297,6 +269,36 @@
    1.48        "(" $$-- const_type true --$$ ")" >> parens) toks
    1.49    end;
    1.50  
    1.51 +fun mk_old_type_decl ((ts, n), syn) =
    1.52 +  map (fn t => (mk_triple (t, n, syn), false)) ts;
    1.53 +
    1.54 +fun mk_type_decl (((xs, t), None), syn) =
    1.55 +      [(mk_triple (t, string_of_int (length xs), syn), false)]
    1.56 +  | mk_type_decl (((xs, t), Some rhs), syn) =
    1.57 +      [(parens (commas [t, mk_list xs, rhs, syn]), true)];
    1.58 +
    1.59 +fun mk_type_decls tys =
    1.60 +  "|> add_types\n" ^ mk_big_list (keyfilter tys false) ^ "\n\n\
    1.61 +  \|> add_tyabbrs\n" ^ mk_big_list (keyfilter tys true);
    1.62 +
    1.63 +
    1.64 +val old_type_decl = names1 -- nat -- opt_infix >> mk_old_type_decl;
    1.65 +
    1.66 +val type_args =
    1.67 +  type_var >> (fn x => [x]) ||
    1.68 +  "(" $$-- !! (list1 type_var --$$ ")") ||
    1.69 +  empty >> K [];
    1.70 +
    1.71 +val type_decl = type_args -- name --
    1.72 +  optional ("=" $$-- (string || (const_type false >> quote)) >> Some) None
    1.73 +  -- opt_infix >> mk_type_decl;
    1.74 +
    1.75 +val type_decls = repeat1 (old_type_decl || type_decl) >>
    1.76 +                 (mk_type_decls o flat);
    1.77 +
    1.78 +
    1.79 +(* consts *)
    1.80 +
    1.81  val const_decls = repeat1 (names1 --$$ "::" -- !!
    1.82                      ((string || const_type false >> quote) -- opt_mixfix)) >>
    1.83                    (mk_big_list o map mk_triple2 o split_decls);