src/HOL/Tools/Quickcheck/narrowing_generators.ML
changeset 46219 426ed18eba43
parent 46042 ab32a87ba01a
child 46309 693d8d7bc3cd
     1.1 --- a/src/HOL/Tools/Quickcheck/narrowing_generators.ML	Sat Jan 14 20:05:58 2012 +0100
     1.2 +++ b/src/HOL/Tools/Quickcheck/narrowing_generators.ML	Sat Jan 14 21:16:15 2012 +0100
     1.3 @@ -462,7 +462,7 @@
     1.4        let
     1.5          val frees = Term.add_frees t []
     1.6          val t' = fold_rev absfree frees t
     1.7 -        fun wrap f t = list_abs (f (strip_abs t))
     1.8 +        fun wrap f t = uncurry (fold_rev Term.abs) (f (strip_abs t))
     1.9          val finitize = if Config.get ctxt finite_functions then wrap finitize_functions else I
    1.10          fun ensure_testable t =
    1.11            Const (@{const_name Quickcheck_Narrowing.ensure_testable}, fastype_of t --> fastype_of t) $ t