src/HOL/Tools/inductive_set_package.ML
changeset 27330 1af2598b5f7d
parent 26988 742e26213212
child 28083 103d9282a946
--- a/src/HOL/Tools/inductive_set_package.ML	Mon Jun 23 20:00:58 2008 +0200
+++ b/src/HOL/Tools/inductive_set_package.ML	Mon Jun 23 23:45:39 2008 +0200
@@ -69,7 +69,7 @@
       fun close p t f =
         let val vs = Term.add_vars t []
         in Drule.instantiate' [] (rev (map (SOME o cterm_of thy o Var) vs))
-          (p (fold (fn x as (_, T) => fn u => all T $ lambda (Var x) u) vs t) f)
+          (p (fold (Logic.all o Var) vs t) f)
         end;
       fun mkop "op &" T x = SOME (Const ("op Int", T --> T --> T), x)
         | mkop "op |" T x = SOME (Const ("op Un", T --> T --> T), x)