--- a/src/FOL/fologic.ML Fri Nov 03 21:31:11 2000 +0100
+++ b/src/FOL/fologic.ML Fri Nov 03 21:31:53 2000 +0100
@@ -9,7 +9,6 @@
sig
val oT : typ
val mk_Trueprop : term -> term
- val atomic_Trueprop : string -> term
val dest_Trueprop : term -> term
val not : term
val conj : term
@@ -44,8 +43,6 @@
fun mk_Trueprop P = Trueprop $ P;
-fun atomic_Trueprop x = mk_Trueprop (Free (x, oT));
-
fun dest_Trueprop (Const ("Trueprop", _) $ P) = P
| dest_Trueprop t = raise TERM ("dest_Trueprop", [t]);
--- 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]);