--- a/src/HOL/hologic.ML Fri Nov 03 21:31:11 2000 +0100
+++ b/src/HOL/hologic.ML Fri Nov 03 21:31:53 2000 +0100
@@ -18,7 +18,6 @@
val mk_setT: typ -> typ
val dest_setT: typ -> typ
val mk_Trueprop: term -> term
- val atomic_Trueprop: string -> term
val dest_Trueprop: term -> term
val conj: term
val disj: term
@@ -106,8 +105,6 @@
fun mk_Trueprop P = Trueprop $ P;
-fun atomic_Trueprop x = mk_Trueprop (Free (x, boolT));
-
fun dest_Trueprop (Const ("Trueprop", _) $ P) = P
| dest_Trueprop t = raise TERM ("dest_Trueprop", [t]);