added dummyS;
authorwenzelm
Tue Nov 14 00:15:43 2006 +0100 (2006-11-14)
changeset 21353cfee13454195
parent 21352 073c79be780c
child 21354 2207380f7576
added dummyS;
src/Pure/term.ML
     1.1 --- a/src/Pure/term.ML	Tue Nov 14 00:15:42 2006 +0100
     1.2 +++ b/src/Pure/term.ML	Tue Nov 14 00:15:43 2006 +0100
     1.3 @@ -30,6 +30,7 @@
     1.4      $ of term * term
     1.5    exception TYPE of string * typ list * term list
     1.6    exception TERM of string * term list
     1.7 +  val dummyS: sort
     1.8    val dummyT: typ
     1.9    val no_dummyT: typ -> typ
    1.10    val --> : typ * typ -> typ
    1.11 @@ -243,7 +244,8 @@
    1.12  
    1.13  (** Types **)
    1.14  
    1.15 -(*dummy type for parsing and printing etc.*)
    1.16 +(*dummies for type-inference etc.*)
    1.17 +val dummyS = [""];
    1.18  val dummyT = Type ("dummy", []);
    1.19  
    1.20  fun no_dummyT typ =