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