# HG changeset patch
# User paulson
# Date 1115887726 -7200
# Node ID dd516176043a40403c35666f32ab22b2b9802f8b
# Parent  902b556e4bc06c4089780f7675fad28c2d0031ca
first-order now ignores "all"

diff -r 902b556e4bc0 -r dd516176043a src/Pure/term.ML
--- a/src/Pure/term.ML	Thu May 12 09:45:54 2005 +0200
+++ b/src/Pure/term.ML	Thu May 12 10:48:46 2005 +0200
@@ -703,8 +703,11 @@
 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.*)
+  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
   | first_order1 Ts t =
       case strip_comb t of
 	       (Var _, ts) => forall (first_order1 Ts andf has_not_funtype Ts) ts
@@ -716,7 +719,6 @@
 
 val is_first_order = first_order1 [];
 
-
 (*Computing the maximum index of a typ*)
 fun maxidx_of_typ(Type(_,Ts)) = maxidx_of_typs Ts
   | maxidx_of_typ(TFree _) = ~1