# 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;