src/HOL/Tools/quickcheck_generators.ML
changeset 33280 e3eaeba6ae28
parent 33243 17014b1b9353
child 33552 506f80a9afe8
     1.1 --- a/src/HOL/Tools/quickcheck_generators.ML	Wed Oct 28 16:27:48 2009 +0100
     1.2 +++ b/src/HOL/Tools/quickcheck_generators.ML	Wed Oct 28 16:28:12 2009 +0100
     1.3 @@ -84,7 +84,7 @@
     1.4      thy
     1.5      |> TheoryTarget.instantiation ([tyco], vs, @{sort random})
     1.6      |> `(fn lthy => Syntax.check_term lthy eq)
     1.7 -    |-> (fn eq => Specification.definition (NONE, (apfst (Binding.conceal) Attrib.empty_binding, eq)))
     1.8 +    |-> (fn eq => Specification.definition (NONE, (apfst Binding.conceal Attrib.empty_binding, eq)))
     1.9      |> snd
    1.10      |> Class.prove_instantiation_exit (K (Class.intro_classes_tac []))
    1.11    end;
    1.12 @@ -177,7 +177,7 @@
    1.13          val proj_eqs = map2 (fn v => fn proj => (v, lambda arg proj)) vs projs;
    1.14          val proj_defs = map2 (fn Free (name, _) => fn (_, rhs) =>
    1.15            ((Binding.conceal (Binding.name name), NoSyn),
    1.16 -            (apfst (Binding.conceal) Attrib.empty_binding, rhs))) vs proj_eqs;
    1.17 +            (apfst Binding.conceal Attrib.empty_binding, rhs))) vs proj_eqs;
    1.18          val aux_eq' = Pattern.rewrite_term thy proj_eqs [] aux_eq;
    1.19          fun prove_eqs aux_simp proj_defs lthy = 
    1.20            let
    1.21 @@ -305,7 +305,7 @@
    1.22      |> random_aux_specification prfx random_auxN auxs_eqs
    1.23      |> `(fn lthy => map (Syntax.check_term lthy) random_defs)
    1.24      |-> (fn random_defs' => fold_map (fn random_def =>
    1.25 -          Specification.definition (NONE, (apfst (Binding.conceal)
    1.26 +          Specification.definition (NONE, (apfst Binding.conceal
    1.27              Attrib.empty_binding, random_def))) random_defs')
    1.28      |> snd
    1.29      |> Class.prove_instantiation_exit (K (Class.intro_classes_tac []))