--- a/src/HOL/Tools/Sledgehammer/metis_clauses.ML Tue Jun 29 11:20:05 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/metis_clauses.ML Tue Jun 29 11:29:31 2010 +0200
@@ -66,6 +66,7 @@
val literals_of_term : theory -> term -> literal list * typ list
val conceal_skolem_terms :
int -> (string * term) list -> term -> (string * term) list * term
+ val reveal_skolem_terms : (string * term) list -> term -> term
val tfree_classes_of_terms : term list -> string list
val tvar_classes_of_terms : term list -> string list
val type_consts_of_terms : theory -> term list -> string list
@@ -473,6 +474,15 @@
else
(skolems, t)
+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)
+
(***************************************************************)
(* Type Classes Present in the Axiom or Conjecture Clauses *)
--- 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