# HG changeset patch
# User wenzelm
# Date 1163459743 -3600
# Node ID cfee1345419507e3ca770f2c90124477e0bb3b62
# Parent  073c79be780c170cc79bf1ea7880611166c8449a
added dummyS;

diff -r 073c79be780c -r cfee13454195 src/Pure/term.ML
--- 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 =