# HG changeset patch # User wenzelm # Date 1006986538 -3600 # Node ID e2cb7e8bb03794abc581d5e1cef5a3705c29ab9a # Parent f0f06950820d5d87699d0f32c010a8cefdcbba10 Syntax.read_typ: pass intern sort fn; diff -r f0f06950820d -r e2cb7e8bb037 src/Pure/sign.ML --- a/src/Pure/sign.ML Wed Nov 28 23:27:35 2001 +0100 +++ b/src/Pure/sign.ML Wed Nov 28 23:28:58 2001 +0100 @@ -591,7 +591,7 @@ fun rd_raw_typ syn tsig spaces def_sort str = intrn_tycons spaces - (Syntax.read_typ syn (Type.get_sort tsig def_sort (intrn_sort spaces)) str + (Syntax.read_typ syn (Type.get_sort tsig def_sort (intrn_sort spaces)) (intrn_sort spaces) str handle ERROR => err_in_type str); fun read_raw_typ' syn (sg as Sg (_, {tsig, spaces, ...}), def_sort) str =