src/HOL/Code_Evaluation.thy
changeset 35845 e5980f0ad025
parent 35366 6d474096698c
child 36176 3fe7e97ccca8
     1.1 --- a/src/HOL/Code_Evaluation.thy	Sat Mar 20 02:23:41 2010 +0100
     1.2 +++ b/src/HOL/Code_Evaluation.thy	Sat Mar 20 17:33:11 2010 +0100
     1.3 @@ -87,13 +87,14 @@
     1.4      let
     1.5        val t = list_comb (Const (c, tys ---> ty),
     1.6          map Free (Name.names Name.context "a" tys));
     1.7 -      val (arg, rhs) = pairself (Thm.cterm_of thy o map_types Logic.unvarifyT o Logic.varify)
     1.8 -        (t, (map_aterms (fn t as Free (v, ty) => HOLogic.mk_term_of ty t | t => t) o HOLogic.reflect_term) t)
     1.9 +      val (arg, rhs) =
    1.10 +        pairself (Thm.cterm_of thy o map_types Logic.unvarifyT_global o Logic.varify_global)
    1.11 +          (t, (map_aterms (fn t as Free (v, ty) => HOLogic.mk_term_of ty t | t => t) o HOLogic.reflect_term) t)
    1.12        val cty = Thm.ctyp_of thy ty;
    1.13      in
    1.14        @{thm term_of_anything}
    1.15        |> Drule.instantiate' [SOME cty] [SOME arg, SOME rhs]
    1.16 -      |> Thm.varifyT
    1.17 +      |> Thm.varifyT_global
    1.18      end;
    1.19    fun add_term_of_code tyco raw_vs raw_cs thy =
    1.20      let
    1.21 @@ -131,7 +132,7 @@
    1.22      in
    1.23        @{thm term_of_anything}
    1.24        |> Drule.instantiate' [SOME cty] [SOME (Thm.cterm_of thy arg), SOME rhs]
    1.25 -      |> Thm.varifyT
    1.26 +      |> Thm.varifyT_global
    1.27      end;
    1.28    fun add_term_of_code tyco raw_vs abs raw_ty_rep proj thy =
    1.29      let