# HG changeset patch
# User wenzelm
# Date 1150234919 -7200
# Node ID d064712bdd1dd40cc8d83c2ba829d2d71593c09a
# Parent  0817ba18231e021bdd9735ca5ee1d38beeac8487
avoid global Drule.unvarify;

diff -r 0817ba18231e -r d064712bdd1d src/Pure/Tools/codegen_theorems.ML
--- a/src/Pure/Tools/codegen_theorems.ML	Tue Jun 13 23:41:58 2006 +0200
+++ b/src/Pure/Tools/codegen_theorems.ML	Tue Jun 13 23:41:59 2006 +0200
@@ -578,6 +578,9 @@
 fun tap_typ thy [] = NONE
   | tap_typ thy (thms as (thm::_)) = SOME (extr_typ thy thm, thms);
 
+fun unvarify thy thms =
+  #1 (ProofContext.import true thms (ProofContext.init thy));
+
 fun preprocess thy thms =
   let
     fun burrow_thms f [] = []
@@ -618,8 +621,7 @@
         #> debug_msg (string_of_thm)
         #> Drule.zero_var_indexes
        )
-    |> map Drule.unvarifyT
-    |> map Drule.unvarify
+    |> unvarify thy
     |> tap_typ thy
   end;