diff -r b63b21f370ca -r 7d13a5ace928 src/FOL/fologic.ML
--- a/src/FOL/fologic.ML	Sun Jul 30 13:01:50 2000 +0200
+++ b/src/FOL/fologic.ML	Sun Jul 30 13:02:14 2000 +0200
@@ -9,6 +9,7 @@
 sig
   val oT		: typ
   val mk_Trueprop	: term -> term
+  val atomic_Trueprop	: string -> term
   val dest_Trueprop	: term -> term
   val conj		: term
   val disj		: term
@@ -36,6 +37,8 @@
 
 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]);