summary |
shortlog |
changelog |
graph |
tags |
branches |
files |
changeset |
file |
revisions |
annotate |
diff |
raw

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