--- a/src/HOL/Tools/Sledgehammer/metis_tactics.ML Tue Jun 29 11:20:05 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/metis_tactics.ML Tue Jun 29 11:29:31 2010 +0200
@@ -235,15 +235,6 @@
SOME tf => mk_tfree ctxt tf
| NONE => raise Fail ("fol_type_to_isa: " ^ x));
-fun reveal_skolem_terms skolems =
- map_aterms (fn t as Const (s, _) =>
- if String.isPrefix skolem_theory_name s then
- AList.lookup (op =) skolems s |> the
- |> map_types Type_Infer.paramify_vars
- else
- t
- | t => t)
-
(*Maps metis terms to isabelle terms*)
fun hol_term_from_fol_PT ctxt fol_tm =
let val thy = ProofContext.theory_of ctxt