src/HOL/Tools/hologic.ML
changeset 56254 a2dd9200854d
parent 55414 eab03e9cee8a
child 59058 a78612c67ec0
     1.1 --- a/src/HOL/Tools/hologic.ML	Sat Mar 22 18:16:54 2014 +0100
     1.2 +++ b/src/HOL/Tools/hologic.ML	Sat Mar 22 18:19:57 2014 +0100
     1.3 @@ -6,8 +6,6 @@
     1.4  
     1.5  signature HOLOGIC =
     1.6  sig
     1.7 -  val typeS: sort
     1.8 -  val typeT: typ
     1.9    val id_const: typ -> term
    1.10    val mk_comp: term * term -> term
    1.11    val boolN: string
    1.12 @@ -141,12 +139,6 @@
    1.13  structure HOLogic: HOLOGIC =
    1.14  struct
    1.15  
    1.16 -(* HOL syntax *)
    1.17 -
    1.18 -val typeS: sort = ["HOL.type"];
    1.19 -val typeT = Type_Infer.anyT typeS;
    1.20 -
    1.21 -
    1.22  (* functions *)
    1.23  
    1.24  fun id_const T = Const ("Fun.id", T --> T);