src/Pure/term.ML
changeset 15954 dd516176043a
parent 15914 2a8f86685745
child 15962 a3288211965a
     1.1 --- a/src/Pure/term.ML	Thu May 12 09:45:54 2005 +0200
     1.2 +++ b/src/Pure/term.ML	Thu May 12 10:48:46 2005 +0200
     1.3 @@ -703,8 +703,11 @@
     1.4  fun has_not_funtype Ts t = not (is_funtype (fastype_of1 (Ts,t)));
     1.5  
     1.6  (*First order means in all terms of the form f(t1,...,tn) no argument has a function
     1.7 -  type.*)
     1.8 +  type. The meta-quantifier "all" is excluded--its argument always has a function
     1.9 +  type--through a recursive call into its body.*)
    1.10  fun first_order1 Ts (Abs (_,T,body)) = first_order1 (T::Ts) body
    1.11 +  | first_order1 Ts (Const("all",_)$Abs(a,T,body)) = 
    1.12 +      not (is_funtype T) andalso first_order1 (T::Ts) body
    1.13    | first_order1 Ts t =
    1.14        case strip_comb t of
    1.15  	       (Var _, ts) => forall (first_order1 Ts andf has_not_funtype Ts) ts
    1.16 @@ -716,7 +719,6 @@
    1.17  
    1.18  val is_first_order = first_order1 [];
    1.19  
    1.20 -
    1.21  (*Computing the maximum index of a typ*)
    1.22  fun maxidx_of_typ(Type(_,Ts)) = maxidx_of_typs Ts
    1.23    | maxidx_of_typ(TFree _) = ~1