# HG changeset patch
# User wenzelm
# Date 973283513 -3600
# Node ID a499b9ce2ffecedc54867970af37ddd5090e01b5
# Parent  a092ae7bb2a6865f084f6bf4a07b42fea088b484
removed atomic_Trueprop (now in Pure/Isar/auto_bind.ML);

diff -r a092ae7bb2a6 -r a499b9ce2ffe 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]);
 
diff -r a092ae7bb2a6 -r a499b9ce2ffe src/HOL/hologic.ML
--- 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]);