added type class to simple_type
authorclasohm
Wed Nov 29 16:47:38 1995 +0100 (1995-11-29)
changeset 13712f97fc253763
parent 1370 7361ac9b024d
child 1372 16330e3fa3b7
added type class to simple_type
src/Pure/Thy/thy_parse.ML
     1.1 --- a/src/Pure/Thy/thy_parse.ML	Wed Nov 29 16:44:59 1995 +0100
     1.2 +++ b/src/Pure/Thy/thy_parse.ML	Wed Nov 29 16:47:38 1995 +0100
     1.3 @@ -259,7 +259,9 @@
     1.4  
     1.5  (* consts *)
     1.6  
     1.7 -val simple_type = ident || kind TypeVar;
     1.8 +val simple_type = ident ||
     1.9 +  (kind TypeVar -- optional ("::" $$-- ident >> cat "::") "" >>
    1.10 +   (fn (tv, cl) => tv ^ cl));
    1.11  
    1.12  (*Types with type arguments, like e.g. "'a list list"*)
    1.13  fun complex_type toks =
    1.14 @@ -274,7 +276,7 @@
    1.15  (*Const type which is limited at the end by "=>", ")", "]" or ","*)
    1.16  fun param_type toks =
    1.17    ((complex_type || "(" $$-- param_type --$$ ")" >> parens ||
    1.18 -    "[" $$-- !! (list1 param_type) --$$ "]" >> mk_list) --
    1.19 +    "[" $$-- (list1 param_type) --$$ "]" >> mk_list) --
    1.20       repeat ("=>" $$-- param_type >> cat " =>") >>
    1.21       (fn (t, ts) => t ^ implode ts)) toks;
    1.22