src/Pure/logic.ML
changeset 23357 16e0ec4bcd81
parent 23238 3de6e253efc4
child 23418 c195f6f13769
     1.1 --- a/src/Pure/logic.ML	Wed Jun 13 00:01:59 2007 +0200
     1.2 +++ b/src/Pure/logic.ML	Wed Jun 13 00:02:00 2007 +0200
     1.3 @@ -8,7 +8,6 @@
     1.4  
     1.5  signature LOGIC =
     1.6  sig
     1.7 -  val is_atomic: term -> bool
     1.8    val dest_all: term -> typ * term
     1.9    val mk_equals: term * term -> term
    1.10    val dest_equals: term -> term * term
    1.11 @@ -88,11 +87,6 @@
    1.12  
    1.13  (*** Abstract syntax operations on the meta-connectives ***)
    1.14  
    1.15 -fun is_atomic (Const ("==>", _) $ _ $ _) = false
    1.16 -  | is_atomic (Const ("all", _) $ _) = false
    1.17 -  | is_atomic _ = true;
    1.18 -
    1.19 -
    1.20  (** all **)
    1.21  
    1.22  fun dest_all (Const ("all", Type ("fun", [Type ("fun", [T, _]), _])) $ A) = (T, A)