--- a/src/HOL/Tools/hologic.ML Fri Dec 02 14:37:25 2011 +0100
+++ b/src/HOL/Tools/hologic.ML Fri Dec 02 14:54:25 2011 +0100
@@ -15,8 +15,6 @@
val Trueprop: term
val mk_Trueprop: term -> term
val dest_Trueprop: term -> term
- val true_const: term
- val false_const: term
val mk_induct_forall: typ -> term
val mk_setT: typ -> typ
val dest_setT: typ -> typ
@@ -162,9 +160,6 @@
val boolN = "HOL.bool";
val boolT = Type (boolN, []);
-val true_const = Const ("HOL.True", boolT);
-val false_const = Const ("HOL.False", boolT);
-
fun mk_induct_forall T = Const ("HOL.induct_forall", (T --> boolT) --> boolT);
fun mk_setT T = T --> boolT;