# HG changeset patch
# User boehmes
# Date 1270759146 -7200
# Node ID 7e1f972df25fdb84386fbdfca37ac2389a9206d3
# Parent  53992c639da5aeed1d1694e1d05219be3e5cdfc0
added missing case: meta universal quantifier

diff -r 53992c639da5 -r 7e1f972df25f src/HOL/Tools/Qelim/ferrante_rackoff.ML
--- a/src/HOL/Tools/Qelim/ferrante_rackoff.ML	Thu Apr 08 08:17:27 2010 +0200
+++ b/src/HOL/Tools/Qelim/ferrante_rackoff.ML	Thu Apr 08 22:39:06 2010 +0200
@@ -187,6 +187,7 @@
    | Const ("op -->", _) $ _ $ _ => find_args bounds tm
    | Const ("==>", _) $ _ $ _ => find_args bounds tm
    | Const ("==", _) $ _ $ _ => find_args bounds tm
+   | Const ("all", _) $ _ => find_body bounds (Thm.dest_arg tm)
    | Const ("Trueprop", _) $ _ => h bounds (Thm.dest_arg tm)
    | _ => Thm.dest_fun2 tm)
   and find_args bounds tm =