# HG changeset patch
# User wenzelm
# Date 855247639 -3600
# Node ID c7a0c0618ca0f42ad4c7a533a9cddd765800f3a8
# Parent  8b92caca102c7fd8735ac09325784b07b90b1bf4
adapted to new Syntax.read_typ;

diff -r 8b92caca102c -r c7a0c0618ca0 src/Pure/sign.ML
--- a/src/Pure/sign.ML	Thu Feb 06 17:46:22 1997 +0100
+++ b/src/Pure/sign.ML	Thu Feb 06 17:47:19 1997 +0100
@@ -235,7 +235,7 @@
   error ("The error(s) above occurred in type " ^ quote s);
 
 fun read_raw_typ syn tsig sort_of str =
-  Syntax.read_typ syn (fn x => if_none (sort_of x) (Type.defaultS tsig)) str
+  Syntax.read_typ syn (Type.eq_sort tsig) (Type.get_sort tsig sort_of) str
     handle ERROR => err_in_type str;
 
 (*read and certify typ wrt a signature*)