src/HOL/Tools/Quickcheck/narrowing_generators.ML
changeset 60801 7664e0916eec
parent 59621 291934bac95e
child 60956 10d463883dc2
     1.1 --- a/src/HOL/Tools/Quickcheck/narrowing_generators.ML	Mon Jul 27 16:35:12 2015 +0200
     1.2 +++ b/src/HOL/Tools/Quickcheck/narrowing_generators.ML	Mon Jul 27 17:44:55 2015 +0200
     1.3 @@ -80,7 +80,7 @@
     1.4      val cty = Thm.global_ctyp_of thy ty;
     1.5    in
     1.6      @{thm partial_term_of_anything}
     1.7 -    |> Drule.instantiate' [SOME cty] insts
     1.8 +    |> Thm.instantiate' [SOME cty] insts
     1.9      |> Thm.varifyT_global
    1.10    end
    1.11  
    1.12 @@ -99,7 +99,7 @@
    1.13            @{term "Code_Evaluation.Free (STR ''_'')"} $ HOLogic.mk_typerep ty];
    1.14      val var_eq =
    1.15        @{thm partial_term_of_anything}
    1.16 -      |> Drule.instantiate' [SOME (Thm.global_ctyp_of thy ty)] var_insts
    1.17 +      |> Thm.instantiate' [SOME (Thm.global_ctyp_of thy ty)] var_insts
    1.18        |> Thm.varifyT_global
    1.19      val eqs = var_eq :: map_index (mk_partial_term_of_eq thy ty) cs;
    1.20   in