src/HOL/Tools/Quickcheck/narrowing_generators.ML
changeset 59621 291934bac95e
parent 59498 50b60f501b05
child 60801 7664e0916eec
     1.1 --- a/src/HOL/Tools/Quickcheck/narrowing_generators.ML	Fri Mar 06 14:01:08 2015 +0100
     1.2 +++ b/src/HOL/Tools/Quickcheck/narrowing_generators.ML	Fri Mar 06 15:58:56 2015 +0100
     1.3 @@ -75,9 +75,9 @@
     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 Logic.unvarify_types_global o Logic.varify_global)
     1.8 +      map (SOME o Thm.global_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 +    val cty = Thm.global_ctyp_of thy ty;
    1.12    in
    1.13      @{thm partial_term_of_anything}
    1.14      |> Drule.instantiate' [SOME cty] insts
    1.15 @@ -94,12 +94,12 @@
    1.16        (fn TFree (v, _) => TFree (v, (the o AList.lookup (op =) vs) v)) raw_cs;
    1.17      val const = Axclass.param_of_inst thy (@{const_name partial_term_of}, tyco);
    1.18      val var_insts =
    1.19 -      map (SOME o Thm.cterm_of thy o Logic.unvarify_types_global o Logic.varify_global)
    1.20 +      map (SOME o Thm.global_cterm_of thy o Logic.unvarify_types_global o Logic.varify_global)
    1.21          [Free ("ty", Term.itselfT ty), @{term "Quickcheck_Narrowing.Narrowing_variable p tt"},
    1.22            @{term "Code_Evaluation.Free (STR ''_'')"} $ HOLogic.mk_typerep ty];
    1.23      val var_eq =
    1.24        @{thm partial_term_of_anything}
    1.25 -      |> Drule.instantiate' [SOME (Thm.ctyp_of thy ty)] var_insts
    1.26 +      |> Drule.instantiate' [SOME (Thm.global_ctyp_of thy ty)] var_insts
    1.27        |> Thm.varifyT_global
    1.28      val eqs = var_eq :: map_index (mk_partial_term_of_eq thy ty) cs;
    1.29   in