diff -r ac9d126456e1 -r 3de6e253efc4 src/Pure/logic.ML
--- a/src/Pure/logic.ML	Mon Jun 04 21:04:19 2007 +0200
+++ b/src/Pure/logic.ML	Mon Jun 04 21:04:19 2007 +0200
@@ -8,7 +8,7 @@
 
 signature LOGIC =
 sig
-  val is_all: term -> bool
+  val is_atomic: term -> bool
   val dest_all: term -> typ * term
   val mk_equals: term * term -> term
   val dest_equals: term -> term * term
@@ -88,10 +88,12 @@
 
 (*** Abstract syntax operations on the meta-connectives ***)
 
-(** all **)
+fun is_atomic (Const ("==>", _) $ _ $ _) = false
+  | is_atomic (Const ("all", _) $ _) = false
+  | is_atomic _ = true;
 
-fun is_all (Const ("all", _) $ _) = true
-  | is_all _ = false;
+
+(** all **)
 
 fun dest_all (Const ("all", Type ("fun", [Type ("fun", [T, _]), _])) $ A) = (T, A)
   | dest_all t = raise TERM ("dest_all", [t]);