# HG changeset patch
# User blanchet
# Date 1306916983 -7200
# Node ID a3f3b7a0e99ebdb98a46bad22ffcaffa5a1d3be3
# Parent  a7db0afd520048b415e7ce6079fb7c38d1a9e438
export one more function

diff -r a7db0afd5200 -r a3f3b7a0e99e src/HOL/Tools/ATP/atp_reconstruct.ML
--- a/src/HOL/Tools/ATP/atp_reconstruct.ML	Wed Jun 01 10:29:43 2011 +0200
+++ b/src/HOL/Tools/ATP/atp_reconstruct.ML	Wed Jun 01 10:29:43 2011 +0200
@@ -9,6 +9,7 @@
 signature ATP_RECONSTRUCT =
 sig
   type 'a fo_term = 'a ATP_Problem.fo_term
+  type ('a, 'b, 'c) formula = ('a, 'b, 'c) ATP_Problem.formula
   type 'a proof = 'a ATP_Proof.proof
   type locality = ATP_Translate.locality
   type type_sys = ATP_Translate.type_sys
@@ -45,6 +46,9 @@
   val term_from_atp :
     theory -> bool -> int Symtab.table -> (string * sort) list -> typ option
     -> string fo_term -> term
+  val prop_from_atp :
+    theory -> bool -> int Symtab.table -> (string * sort) list
+    -> (string, string, string fo_term) formula -> term
   val isar_proof_text :
     Proof.context -> bool -> isar_params -> one_line_params -> string
   val proof_text :
@@ -536,7 +540,7 @@
 
 (* Interpret an ATP formula as a HOL term, extracting sort constraints as they
    appear in the formula. *)
-fun prop_from_formula thy textual sym_tab tfrees phi =
+fun prop_from_atp thy textual sym_tab tfrees phi =
   let
     fun do_formula pos phi =
       case phi of
@@ -577,11 +581,11 @@
 fun decode_line sym_tab tfrees (Definition (name, phi1, phi2)) ctxt =
     let
       val thy = Proof_Context.theory_of ctxt
-      val t1 = prop_from_formula thy true sym_tab tfrees phi1
+      val t1 = prop_from_atp thy true sym_tab tfrees phi1
       val vars = snd (strip_comb t1)
       val frees = map unvarify_term vars
       val unvarify_args = subst_atomic (vars ~~ frees)
-      val t2 = prop_from_formula thy true sym_tab tfrees phi2
+      val t2 = prop_from_atp thy true sym_tab tfrees phi2
       val (t1, t2) =
         HOLogic.eq_const HOLogic.typeT $ t1 $ t2
         |> unvarify_args |> uncombine_term thy |> check_formula ctxt
@@ -593,7 +597,7 @@
   | decode_line sym_tab tfrees (Inference (name, u, deps)) ctxt =
     let
       val thy = Proof_Context.theory_of ctxt
-      val t = u |> prop_from_formula thy true sym_tab tfrees
+      val t = u |> prop_from_atp thy true sym_tab tfrees
                 |> uncombine_term thy |> check_formula ctxt
     in
       (Inference (name, t, deps),