src/FOL/fologic.ML

--- 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]);