# HG changeset patch # User kleing # Date 1116224896 -7200 # Node ID a3288211965a3db4d22effe74a8d0defdb3f24eb # Parent 24c6b96b4a2f6b2f64f4ba54db7f0f33153cb2b4 line wrap diff -r 24c6b96b4a2f -r a3288211965a src/Pure/term.ML --- a/src/Pure/term.ML Sun May 15 21:04:10 2005 +0200 +++ b/src/Pure/term.ML Mon May 16 08:28:16 2005 +0200 @@ -702,9 +702,9 @@ (*Argument Ts is a reverse list of binder types, needed if term t contains Bound vars*) fun has_not_funtype Ts t = not (is_funtype (fastype_of1 (Ts,t))); -(*First order means in all terms of the form f(t1,...,tn) no argument has a function - type. The meta-quantifier "all" is excluded--its argument always has a function - type--through a recursive call into its body.*) +(*First order means in all terms of the form f(t1,...,tn) no argument has a + function type. The meta-quantifier "all" is excluded--its argument always + has a function type--through a recursive call into its body.*) fun first_order1 Ts (Abs (_,T,body)) = first_order1 (T::Ts) body | first_order1 Ts (Const("all",_)$Abs(a,T,body)) = not (is_funtype T) andalso first_order1 (T::Ts) body