src/HOL/Tools/Quickcheck/narrowing_generators.ML
changeset 44241 7943b69f0188
parent 43915 ef347714c5c1
child 44272 360fcbb1aa01
     1.1 --- a/src/HOL/Tools/Quickcheck/narrowing_generators.ML	Wed Aug 17 16:46:58 2011 +0200
     1.2 +++ b/src/HOL/Tools/Quickcheck/narrowing_generators.ML	Wed Aug 17 18:05:31 2011 +0200
     1.3 @@ -340,10 +340,11 @@
     1.4        in
     1.5          case dT of
     1.6            Type (@{type_name fun}, _) =>
     1.7 -            (fn t => absdummy (dT, rt' (mk_eval_cfun dT rT' $ incr_boundvars 1 t $ Bound 0)),
     1.8 -            Type (@{type_name "Quickcheck_Narrowing.cfun"}, [rT']))
     1.9 -        | _ => (fn t => absdummy (dT, rt' (mk_eval_ffun dT rT' $ incr_boundvars 1 t $ Bound 0)),
    1.10 -            Type (@{type_name "Quickcheck_Narrowing.ffun"}, [dT, rT']))
    1.11 +            (fn t => absdummy dT (rt' (mk_eval_cfun dT rT' $ incr_boundvars 1 t $ Bound 0)),
    1.12 +              Type (@{type_name "Quickcheck_Narrowing.cfun"}, [rT']))
    1.13 +        | _ =>
    1.14 +            (fn t => absdummy dT (rt' (mk_eval_ffun dT rT' $ incr_boundvars 1 t $ Bound 0)),
    1.15 +              Type (@{type_name "Quickcheck_Narrowing.ffun"}, [dT, rT']))
    1.16        end
    1.17        | eval_function T = (I, T)
    1.18      val (tt, boundTs') = split_list (map eval_function boundTs)
    1.19 @@ -432,7 +433,7 @@
    1.20        end
    1.21      else
    1.22        let
    1.23 -        val t' = Term.list_abs_free (Term.add_frees t [], t)
    1.24 +        val t' = fold_rev absfree (Term.add_frees t []) t
    1.25          fun wrap f t = list_abs (f (strip_abs t))
    1.26          val finitize = if Config.get ctxt finite_functions then wrap finitize_functions else I
    1.27          fun ensure_testable t =