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