# HG changeset patch
# User clasohm
# Date 817660058 -3600
# Node ID 2f97fc253763b0dab70c42ef97f244205d4580b5
# Parent  7361ac9b024d6d1bf2545b2fc5a3ee152c6319a4
added type class to simple_type

diff -r 7361ac9b024d -r 2f97fc253763 src/Pure/Thy/thy_parse.ML
--- a/src/Pure/Thy/thy_parse.ML	Wed Nov 29 16:44:59 1995 +0100
+++ b/src/Pure/Thy/thy_parse.ML	Wed Nov 29 16:47:38 1995 +0100
@@ -259,7 +259,9 @@
 
 (* consts *)
 
-val simple_type = ident || kind TypeVar;
+val simple_type = ident ||
+  (kind TypeVar -- optional ("::" $$-- ident >> cat "::") "" >>
+   (fn (tv, cl) => tv ^ cl));
 
 (*Types with type arguments, like e.g. "'a list list"*)
 fun complex_type toks =
@@ -274,7 +276,7 @@
 (*Const type which is limited at the end by "=>", ")", "]" or ","*)
 fun param_type toks =
   ((complex_type || "(" $$-- param_type --$$ ")" >> parens ||
-    "[" $$-- !! (list1 param_type) --$$ "]" >> mk_list) --
+    "[" $$-- (list1 param_type) --$$ "]" >> mk_list) --
      repeat ("=>" $$-- param_type >> cat " =>") >>
      (fn (t, ts) => t ^ implode ts)) toks;