# HG changeset patch
# User blanchet
# Date 1277803771 -7200
# Node ID df12f798df99ae3d6f462e6979d6de0977c22d20
# Parent  16048a884a2cb77a642660b0cb33e468866f55a3
move function

diff -r 16048a884a2c -r df12f798df99 src/HOL/Tools/Sledgehammer/metis_clauses.ML
--- 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     *)
diff -r 16048a884a2c -r df12f798df99 src/HOL/Tools/Sledgehammer/metis_tactics.ML
--- 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