# HG changeset patch
# User wenzelm
# Date 1181685720 -7200
# Node ID 16e0ec4bcd8175e8ca76c3f36bb857671d64497b
# Parent  dbe3731241c3cbfc851ad207654ff3f447bcda67
removed unused is_atomic;

diff -r dbe3731241c3 -r 16e0ec4bcd81 src/Pure/logic.ML
--- a/src/Pure/logic.ML	Wed Jun 13 00:01:59 2007 +0200
+++ b/src/Pure/logic.ML	Wed Jun 13 00:02:00 2007 +0200
@@ -8,7 +8,6 @@
 
 signature LOGIC =
 sig
-  val is_atomic: term -> bool
   val dest_all: term -> typ * term
   val mk_equals: term * term -> term
   val dest_equals: term -> term * term
@@ -88,11 +87,6 @@
 
 (*** Abstract syntax operations on the meta-connectives ***)
 
-fun is_atomic (Const ("==>", _) $ _ $ _) = false
-  | is_atomic (Const ("all", _) $ _) = false
-  | is_atomic _ = true;
-
-
 (** all **)
 
 fun dest_all (Const ("all", Type ("fun", [Type ("fun", [T, _]), _])) $ A) = (T, A)