src/HOL/Tools/Quickcheck/narrowing_generators.ML
changeset 45344 e209da839ff4
parent 45159 3f1d1ce024cb
child 45418 e5ef7aa77fde
     1.1 --- a/src/HOL/Tools/Quickcheck/narrowing_generators.ML	Sat Nov 05 10:59:11 2011 +0100
     1.2 +++ b/src/HOL/Tools/Quickcheck/narrowing_generators.ML	Sat Nov 05 15:00:49 2011 +0100
     1.3 @@ -75,7 +75,7 @@
     1.4          (map mk_partial_term_of (frees ~~ tys))
     1.5          (@{term "Code_Evaluation.Const"} $ HOLogic.mk_literal c $ HOLogic.mk_typerep (tys ---> ty))
     1.6      val insts =
     1.7 -      map (SOME o Thm.cterm_of thy o map_types Logic.unvarifyT_global o Logic.varify_global)
     1.8 +      map (SOME o Thm.cterm_of thy o Logic.unvarify_types_global o Logic.varify_global)
     1.9          [Free ("ty", Term.itselfT ty), narrowing_term, rhs]
    1.10      val cty = Thm.ctyp_of thy ty;
    1.11    in
    1.12 @@ -93,9 +93,10 @@
    1.13      val cs = (map o apsnd o apsnd o map o map_atyps)
    1.14        (fn TFree (v, _) => TFree (v, (the o AList.lookup (op =) vs) v)) raw_cs;
    1.15      val const = AxClass.param_of_inst thy (@{const_name partial_term_of}, tyco);
    1.16 -    val var_insts = map (SOME o Thm.cterm_of thy o map_types Logic.unvarifyT_global o Logic.varify_global)
    1.17 +    val var_insts =
    1.18 +      map (SOME o Thm.cterm_of thy o Logic.unvarify_types_global o Logic.varify_global)
    1.19          [Free ("ty", Term.itselfT ty), @{term "Quickcheck_Narrowing.Var p tt"},
    1.20 -          @{term "Code_Evaluation.Free (STR ''_'')"} $ HOLogic.mk_typerep ty]
    1.21 +          @{term "Code_Evaluation.Free (STR ''_'')"} $ HOLogic.mk_typerep ty];
    1.22      val var_eq =
    1.23        @{thm partial_term_of_anything}
    1.24        |> Drule.instantiate' [SOME (Thm.ctyp_of thy ty)] var_insts