src/HOL/Code_Evaluation.thy
changeset 35845 e5980f0ad025
parent 35366 6d474096698c
child 36176 3fe7e97ccca8
--- a/src/HOL/Code_Evaluation.thy	Sat Mar 20 02:23:41 2010 +0100
+++ b/src/HOL/Code_Evaluation.thy	Sat Mar 20 17:33:11 2010 +0100
@@ -87,13 +87,14 @@
     let
       val t = list_comb (Const (c, tys ---> ty),
         map Free (Name.names Name.context "a" tys));
-      val (arg, rhs) = pairself (Thm.cterm_of thy o map_types Logic.unvarifyT o Logic.varify)
-        (t, (map_aterms (fn t as Free (v, ty) => HOLogic.mk_term_of ty t | t => t) o HOLogic.reflect_term) t)
+      val (arg, rhs) =
+        pairself (Thm.cterm_of thy o map_types Logic.unvarifyT_global o Logic.varify_global)
+          (t, (map_aterms (fn t as Free (v, ty) => HOLogic.mk_term_of ty t | t => t) o HOLogic.reflect_term) t)
       val cty = Thm.ctyp_of thy ty;
     in
       @{thm term_of_anything}
       |> Drule.instantiate' [SOME cty] [SOME arg, SOME rhs]
-      |> Thm.varifyT
+      |> Thm.varifyT_global
     end;
   fun add_term_of_code tyco raw_vs raw_cs thy =
     let
@@ -131,7 +132,7 @@
     in
       @{thm term_of_anything}
       |> Drule.instantiate' [SOME cty] [SOME (Thm.cterm_of thy arg), SOME rhs]
-      |> Thm.varifyT
+      |> Thm.varifyT_global
     end;
   fun add_term_of_code tyco raw_vs abs raw_ty_rep proj thy =
     let