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.
added dummyS;
authorwenzelm
Tue, 14 Nov 2006 00:15:43 +0100
changeset 21353 cfee13454195
parent 21352 073c79be780c
child 21354 2207380f7576
added dummyS;
src/Pure/term.ML file | annotate | diff | comparison | revisions 
--- a/src/Pure/term.ML	Tue Nov 14 00:15:42 2006 +0100
+++ b/src/Pure/term.ML	Tue Nov 14 00:15:43 2006 +0100
@@ -30,6 +30,7 @@
     $ of term * term
   exception TYPE of string * typ list * term list
   exception TERM of string * term list
+  val dummyS: sort
   val dummyT: typ
   val no_dummyT: typ -> typ
   val --> : typ * typ -> typ
@@ -243,7 +244,8 @@
 
 (** Types **)
 
-(*dummy type for parsing and printing etc.*)
+(*dummies for type-inference etc.*)
+val dummyS = [""];
 val dummyT = Type ("dummy", []);
 
 fun no_dummyT typ =
isabelle