src/Pure/term.ML
changeset 15962 a3288211965a
parent 15954 dd516176043a
child 15986 db3cd4fa9b19
     1.1 --- a/src/Pure/term.ML	Sun May 15 21:04:10 2005 +0200
     1.2 +++ b/src/Pure/term.ML	Mon May 16 08:28:16 2005 +0200
     1.3 @@ -702,9 +702,9 @@
     1.4  (*Argument Ts is a reverse list of binder types, needed if term t contains Bound vars*)
     1.5  fun has_not_funtype Ts t = not (is_funtype (fastype_of1 (Ts,t)));
     1.6  
     1.7 -(*First order means in all terms of the form f(t1,...,tn) no argument has a function
     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 +(*First order means in all terms of the form f(t1,...,tn) no argument has a 
    1.11 +  function type. The meta-quantifier "all" is excluded--its argument always 
    1.12 +  has a function type--through a recursive call into its body.*)
    1.13  fun first_order1 Ts (Abs (_,T,body)) = first_order1 (T::Ts) body
    1.14    | first_order1 Ts (Const("all",_)$Abs(a,T,body)) = 
    1.15        not (is_funtype T) andalso first_order1 (T::Ts) body