src/HOL/Tools/hologic.ML

--- a/src/HOL/Tools/hologic.ML	Sat Mar 22 18:16:54 2014 +0100
+++ b/src/HOL/Tools/hologic.ML	Sat Mar 22 18:19:57 2014 +0100
@@ -6,8 +6,6 @@
 
 signature HOLOGIC =
 sig
-  val typeS: sort
-  val typeT: typ
   val id_const: typ -> term
   val mk_comp: term * term -> term
   val boolN: string
@@ -141,12 +139,6 @@
 structure HOLogic: HOLOGIC =
 struct
 
-(* HOL syntax *)
-
-val typeS: sort = ["HOL.type"];
-val typeT = Type_Infer.anyT typeS;
-
-
 (* functions *)
 
 fun id_const T = Const ("Fun.id", T --> T);