# 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 =