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