Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
adapted to new Syntax.read_typ;
authorwenzelm
Thu, 06 Feb 1997 17:47:19 +0100
changeset 2586 c7a0c0618ca0
parent 2585 8b92caca102c
child 2587 ac51a89627ed
adapted to new Syntax.read_typ;
src/Pure/sign.ML file | annotate | diff | comparison | revisions 
--- 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*)
isabelle