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