support readable names even when Isar proof reconstruction is enabled -- useful for debugging
authorblanchet
Sun Apr 25 11:38:46 2010 +0200 (2010-04-25 ago)
changeset 36393be73a2b2443b
parent 36392 c00c57850eb7
child 36394 1a48d18449d8
support readable names even when Isar proof reconstruction is enabled -- useful for debugging
src/HOL/Tools/ATP_Manager/atp_manager.ML
src/HOL/Tools/ATP_Manager/atp_systems.ML
src/HOL/Tools/Sledgehammer/sledgehammer_fact_filter.ML
src/HOL/Tools/Sledgehammer/sledgehammer_fact_minimizer.ML
src/HOL/Tools/Sledgehammer/sledgehammer_fact_preprocessor.ML
src/HOL/Tools/Sledgehammer/sledgehammer_fol_clause.ML
src/HOL/Tools/Sledgehammer/sledgehammer_hol_clause.ML
src/HOL/Tools/Sledgehammer/sledgehammer_proof_reconstruct.ML
     1.1 --- a/src/HOL/Tools/ATP_Manager/atp_manager.ML	Sun Apr 25 10:22:31 2010 +0200
     1.2 +++ b/src/HOL/Tools/ATP_Manager/atp_manager.ML	Sun Apr 25 11:38:46 2010 +0200
     1.3 @@ -8,6 +8,7 @@
     1.4  
     1.5  signature ATP_MANAGER =
     1.6  sig
     1.7 +  type name_pool = Sledgehammer_HOL_Clause.name_pool
     1.8    type relevance_override = Sledgehammer_Fact_Filter.relevance_override
     1.9    type minimize_command = Sledgehammer_Proof_Reconstruct.minimize_command
    1.10    type params =
    1.11 @@ -40,6 +41,7 @@
    1.12    type prover_result =
    1.13      {outcome: failure option,
    1.14       message: string,
    1.15 +     pool: name_pool option,
    1.16       relevant_thm_names: string list,
    1.17       atp_run_time_in_msecs: int,
    1.18       output: string,
    1.19 @@ -102,6 +104,7 @@
    1.20  type prover_result =
    1.21    {outcome: failure option,
    1.22     message: string,
    1.23 +   pool: name_pool option,
    1.24     relevant_thm_names: string list,
    1.25     atp_run_time_in_msecs: int,
    1.26     output: string,
     2.1 --- a/src/HOL/Tools/ATP_Manager/atp_systems.ML	Sun Apr 25 10:22:31 2010 +0200
     2.2 +++ b/src/HOL/Tools/ATP_Manager/atp_systems.ML	Sun Apr 25 11:38:46 2010 +0200
     2.3 @@ -88,6 +88,8 @@
     2.4    | string_for_failure TimedOut = "Timed out."
     2.5    | string_for_failure OutOfResources = "The ATP ran out of resources."
     2.6    | string_for_failure OldSpass =
     2.7 +    (* FIXME: Change the error message below to point to the Isabelle download
     2.8 +       page once the package is there (around the Isabelle2010 release). *)
     2.9      "Warning: Sledgehammer requires a more recent version of SPASS with \
    2.10      \support for the TPTP syntax. To install it, download and untar the \
    2.11      \package \"http://isabelle.in.tum.de/~blanchet/spass-3.7.tgz\" and add the \
    2.12 @@ -193,7 +195,7 @@
    2.13                       else
    2.14                          "") ^ output)
    2.15  
    2.16 -    val (((output, atp_run_time_in_msecs), res_code), _) =
    2.17 +    val (((output, atp_run_time_in_msecs), res_code), pool) =
    2.18        with_path cleanup export run_on (prob_pathname subgoal);
    2.19  
    2.20      (* Check for success and print out some information on failure. *)
    2.21 @@ -201,12 +203,12 @@
    2.22        extract_proof_and_outcome res_code proof_delims known_failures output
    2.23      val (message, relevant_thm_names) =
    2.24        case outcome of
    2.25 -        NONE => proof_text isar_proof debug modulus sorts ctxt
    2.26 +        NONE => proof_text isar_proof pool debug modulus sorts ctxt
    2.27                             (minimize_command, proof, internal_thm_names, th,
    2.28                              subgoal)
    2.29        | SOME failure => (string_for_failure failure ^ "\n", [])
    2.30    in
    2.31 -    {outcome = outcome, message = message,
    2.32 +    {outcome = outcome, message = message, pool = pool,
    2.33       relevant_thm_names = relevant_thm_names,
    2.34       atp_run_time_in_msecs = atp_run_time_in_msecs, output = output,
    2.35       proof = proof, internal_thm_names = internal_thm_names,
    2.36 @@ -228,7 +230,7 @@
    2.37                            higher_order follow_defs max_axiom_clauses
    2.38                            (the_default prefers_theory_relevant theory_relevant))
    2.39        (prepare_clauses higher_order false)
    2.40 -      (write_tptp_file (debug andalso overlord andalso not isar_proof)) home
    2.41 +      (write_tptp_file (debug andalso overlord)) home
    2.42        executable (arguments timeout) proof_delims known_failures name params
    2.43        minimize_command
    2.44  
    2.45 @@ -326,9 +328,6 @@
    2.46     users have upgraded to 3.7, we can kill "spass" (and all DFG support in
    2.47     Sledgehammer) and rename "spass_tptp" "spass". *)
    2.48  
    2.49 -(* FIXME: Change the error message below to point to the Isabelle download
    2.50 -   page once the package is there (around the Isabelle2010 release). *)
    2.51 -
    2.52  val spass_tptp_config =
    2.53    {home = #home spass_config,
    2.54     executable = #executable spass_config,
     3.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_fact_filter.ML	Sun Apr 25 10:22:31 2010 +0200
     3.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_fact_filter.ML	Sun Apr 25 11:38:46 2010 +0200
     3.3 @@ -1,5 +1,6 @@
     3.4  (*  Title:      HOL/Tools/Sledgehammer/sledgehammer_fact_filter.ML
     3.5      Author:     Jia Meng, Cambridge University Computer Laboratory, NICTA
     3.6 +    Author:     Jasmin Blanchette, TU Muenchen
     3.7  *)
     3.8  
     3.9  signature SLEDGEHAMMER_FACT_FILTER =
     4.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_fact_minimizer.ML	Sun Apr 25 10:22:31 2010 +0200
     4.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_fact_minimizer.ML	Sun Apr 25 11:38:46 2010 +0200
     4.3 @@ -92,13 +92,14 @@
     4.4    in
     4.5      (* try prove first to check result and get used theorems *)
     4.6      (case test_thms_fun NONE name_thms_pairs of
     4.7 -      result as {outcome = NONE, internal_thm_names, filtered_clauses, ...} =>
     4.8 +      result as {outcome = NONE, pool, internal_thm_names, filtered_clauses,
     4.9 +                 ...} =>
    4.10          let
    4.11            val used = internal_thm_names |> Vector.foldr (op ::) []
    4.12                                          |> sort_distinct string_ord
    4.13            val to_use =
    4.14              if length used < length name_thms_pairs then
    4.15 -              filter (fn (name1, _) => List.exists (curry (op =) name1) used)
    4.16 +              filter (fn (name1, _) => exists (curry (op =) name1) used)
    4.17                       name_thms_pairs
    4.18              else name_thms_pairs
    4.19            val (min_thms, {proof, internal_thm_names, ...}) =
    4.20 @@ -109,7 +110,7 @@
    4.21              ["Minimized: " ^ string_of_int n ^ " theorem" ^ plural_s n] ^ ".")
    4.22          in
    4.23            (SOME min_thms,
    4.24 -           proof_text isar_proof debug modulus sorts ctxt
    4.25 +           proof_text isar_proof pool debug modulus sorts ctxt
    4.26                        (K "", proof, internal_thm_names, goal, i) |> fst)
    4.27          end
    4.28      | {outcome = SOME TimedOut, ...} =>
     5.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_fact_preprocessor.ML	Sun Apr 25 10:22:31 2010 +0200
     5.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_fact_preprocessor.ML	Sun Apr 25 11:38:46 2010 +0200
     5.3 @@ -1,5 +1,6 @@
     5.4  (*  Title:      HOL/Tools/Sledgehammer/sledgehammer_fact_preprocessor.ML
     5.5      Author:     Jia Meng, Cambridge University Computer Laboratory
     5.6 +    Author:     Jasmin Blanchette, TU Muenchen
     5.7  
     5.8  Transformation of axiom rules (elim/intro/etc) into CNF forms.
     5.9  *)
     6.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_fol_clause.ML	Sun Apr 25 10:22:31 2010 +0200
     6.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_fol_clause.ML	Sun Apr 25 11:38:46 2010 +0200
     6.3 @@ -1,5 +1,6 @@
     6.4  (*  Title:      HOL/Tools/Sledgehammer/sledgehammer_fol_clause.ML
     6.5      Author:     Jia Meng, Cambridge University Computer Laboratory
     6.6 +    Author:     Jasmin Blanchette, TU Muenchen
     6.7  
     6.8  Storing/printing FOL clauses and arity clauses.  Typed equality is
     6.9  treated differently.
     7.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_hol_clause.ML	Sun Apr 25 10:22:31 2010 +0200
     7.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_hol_clause.ML	Sun Apr 25 11:38:46 2010 +0200
     7.3 @@ -8,6 +8,7 @@
     7.4  signature SLEDGEHAMMER_HOL_CLAUSE =
     7.5  sig
     7.6    type name = Sledgehammer_FOL_Clause.name
     7.7 +  type name_pool = Sledgehammer_FOL_Clause.name_pool
     7.8    type kind = Sledgehammer_FOL_Clause.kind
     7.9    type fol_type = Sledgehammer_FOL_Clause.fol_type
    7.10    type classrel_clause = Sledgehammer_FOL_Clause.classrel_clause
    7.11 @@ -37,10 +38,10 @@
    7.12         hol_clause list
    7.13    val write_tptp_file : bool -> bool -> bool -> Path.T ->
    7.14      hol_clause list * hol_clause list * hol_clause list * hol_clause list *
    7.15 -    classrel_clause list * arity_clause list -> unit
    7.16 +    classrel_clause list * arity_clause list -> name_pool option
    7.17    val write_dfg_file : bool -> bool -> Path.T ->
    7.18      hol_clause list * hol_clause list * hol_clause list * hol_clause list *
    7.19 -    classrel_clause list * arity_clause list -> unit
    7.20 +    classrel_clause list * arity_clause list -> name_pool option
    7.21  end
    7.22  
    7.23  structure Sledgehammer_HOL_Clause : SLEDGEHAMMER_HOL_CLAUSE =
    7.24 @@ -500,7 +501,9 @@
    7.25  fun write_tptp_file readable_names full_types explicit_apply file clauses =
    7.26    let
    7.27      fun section _ [] = []
    7.28 -      | section name ss = "\n% " ^ name ^ plural_s (length ss) ^ "\n" :: ss
    7.29 +      | section name ss =
    7.30 +        "\n% " ^ name ^ plural_s (length ss) ^ " (" ^ Int.toString (length ss) ^
    7.31 +        ")\n" :: ss
    7.32      val pool = empty_name_pool readable_names
    7.33      val (conjectures, axclauses, _, helper_clauses,
    7.34        classrel_clauses, arity_clauses) = clauses
    7.35 @@ -515,16 +518,16 @@
    7.36      val arity_clss = map tptp_arity_clause arity_clauses
    7.37      val (helper_clss, pool) = pool_map (apfst fst oo tptp_clause params)
    7.38                                         helper_clauses pool
    7.39 -  in
    7.40 -    File.write_list file
    7.41 -        (header () ::
    7.42 -         section "Relevant fact" ax_clss @
    7.43 -         section "Type variable" tfree_clss @
    7.44 -         section "Conjecture" conjecture_clss @
    7.45 -         section "Class relationship" classrel_clss @
    7.46 -         section "Arity declaration" arity_clss @
    7.47 -         section "Helper fact" helper_clss)
    7.48 -  end
    7.49 +    val _ =
    7.50 +      File.write_list file
    7.51 +          (header () ::
    7.52 +           section "Relevant fact" ax_clss @
    7.53 +           section "Helper fact" helper_clss @
    7.54 +           section "Type variable" tfree_clss @
    7.55 +           section "Conjecture" conjecture_clss @
    7.56 +           section "Class relationship" classrel_clss @
    7.57 +           section "Arity declaration" arity_clss)
    7.58 +  in pool end
    7.59  
    7.60  
    7.61  (* DFG format *)
    7.62 @@ -541,30 +544,30 @@
    7.63      val params = (full_types, explicit_apply, cma, cnh)
    7.64      val ((conjecture_clss, tfree_litss), pool) =
    7.65        pool_map (dfg_clause params) conjectures pool |>> ListPair.unzip
    7.66 -    and probname = Path.implode (Path.base file)
    7.67 +    and problem_name = Path.implode (Path.base file)
    7.68      val (axstrs, pool) = pool_map (apfst fst oo dfg_clause params) axclauses pool
    7.69      val tfree_clss = map dfg_tfree_clause (union_all tfree_litss)
    7.70      val (helper_clauses_strs, pool) =
    7.71        pool_map (apfst fst oo dfg_clause params) helper_clauses pool
    7.72      val (funcs, cl_preds) = decls_of_clauses params (helper_clauses @ conjectures @ axclauses) arity_clauses
    7.73      and ty_preds = preds_of_clauses axclauses classrel_clauses arity_clauses
    7.74 -  in
    7.75 -    File.write_list file
    7.76 -        (header () ::
    7.77 -         string_of_start probname ::
    7.78 -         string_of_descrip probname ::
    7.79 -         string_of_symbols (string_of_funcs funcs)
    7.80 -                           (string_of_preds (cl_preds @ ty_preds)) ::
    7.81 -         "list_of_clauses(axioms, cnf).\n" ::
    7.82 -         axstrs @
    7.83 -         map dfg_classrel_clause classrel_clauses @
    7.84 -         map dfg_arity_clause arity_clauses @
    7.85 -         helper_clauses_strs @
    7.86 -         ["end_of_list.\n\nlist_of_clauses(conjectures, cnf).\n"] @
    7.87 -         tfree_clss @
    7.88 -         conjecture_clss @
    7.89 -         ["end_of_list.\n\n",
    7.90 -          "end_problem.\n"])
    7.91 -  end
    7.92 +    val _ =
    7.93 +      File.write_list file
    7.94 +          (header () ::
    7.95 +           string_of_start problem_name ::
    7.96 +           string_of_descrip problem_name ::
    7.97 +           string_of_symbols (string_of_funcs funcs)
    7.98 +                             (string_of_preds (cl_preds @ ty_preds)) ::
    7.99 +           "list_of_clauses(axioms, cnf).\n" ::
   7.100 +           axstrs @
   7.101 +           map dfg_classrel_clause classrel_clauses @
   7.102 +           map dfg_arity_clause arity_clauses @
   7.103 +           helper_clauses_strs @
   7.104 +           ["end_of_list.\n\nlist_of_clauses(conjectures, cnf).\n"] @
   7.105 +           tfree_clss @
   7.106 +           conjecture_clss @
   7.107 +           ["end_of_list.\n\n",
   7.108 +            "end_problem.\n"])
   7.109 +  in pool end
   7.110  
   7.111  end;
     8.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_proof_reconstruct.ML	Sun Apr 25 10:22:31 2010 +0200
     8.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_proof_reconstruct.ML	Sun Apr 25 11:38:46 2010 +0200
     8.3 @@ -8,6 +8,7 @@
     8.4  signature SLEDGEHAMMER_PROOF_RECONSTRUCT =
     8.5  sig
     8.6    type minimize_command = string list -> string
     8.7 +  type name_pool = Sledgehammer_FOL_Clause.name_pool
     8.8  
     8.9    val chained_hint: string
    8.10    val invert_const: string -> string
    8.11 @@ -20,11 +21,11 @@
    8.12      minimize_command * string * string vector * thm * int
    8.13      -> string * string list
    8.14    val isar_proof_text:
    8.15 -    bool -> int -> bool -> Proof.context
    8.16 +    name_pool option -> bool -> int -> bool -> Proof.context
    8.17      -> minimize_command * string * string vector * thm * int
    8.18      -> string * string list
    8.19    val proof_text:
    8.20 -    bool -> bool -> int -> bool -> Proof.context
    8.21 +    bool -> name_pool option -> bool -> int -> bool -> Proof.context
    8.22      -> minimize_command * string * string vector * thm * int
    8.23      -> string * string list
    8.24  end;
    8.25 @@ -37,18 +38,23 @@
    8.26  
    8.27  type minimize_command = string list -> string
    8.28  
    8.29 -val trace_proof_path = Path.basic "sledgehammer_trace_proof"
    8.30 -
    8.31 -fun trace_proof_msg f =
    8.32 -  if !trace then File.append (File.tmp_path trace_proof_path) (f ()) else ();
    8.33 -
    8.34 -fun string_of_thm ctxt = PrintMode.setmp [] (Display.string_of_thm ctxt);
    8.35 -
    8.36  fun is_ident_char c = Char.isAlphaNum c orelse c = #"_"
    8.37  fun is_head_digit s = Char.isDigit (String.sub (s, 0))
    8.38  
    8.39  fun is_axiom thm_names line_no = line_no <= Vector.length thm_names
    8.40  
    8.41 +fun ugly_name NONE s = s
    8.42 +  | ugly_name (SOME the_pool) s =
    8.43 +    case Symtab.lookup (snd the_pool) s of
    8.44 +      SOME s' => s'
    8.45 +    | NONE => s
    8.46 +
    8.47 +val trace_path = Path.basic "sledgehammer_proof_trace"
    8.48 +fun trace_proof_msg f =
    8.49 +  if !trace then File.append (File.tmp_path trace_path) (f ()) else ();
    8.50 +
    8.51 +val string_of_thm = PrintMode.setmp [] o Display.string_of_thm
    8.52 +
    8.53  (**** PARSING OF TSTP FORMAT ****)
    8.54  
    8.55  (* Syntax trees, either term list or formulae *)
    8.56 @@ -66,52 +72,60 @@
    8.57  val parse_integer = Scan.many1 is_head_digit >> (the o Int.fromString o implode)
    8.58  
    8.59  (* needed for SPASS's output format *)
    8.60 -fun fix_bool_literal "true" = "c_True"
    8.61 -  | fix_bool_literal "false" = "c_False"
    8.62 -fun fix_symbol "equal" = "c_equal"
    8.63 -  | fix_symbol s = s
    8.64 +fun repair_bool_literal "true" = "c_True"
    8.65 +  | repair_bool_literal "false" = "c_False"
    8.66 +fun repair_name pool "equal" = "c_equal"
    8.67 +  | repair_name pool s = ugly_name pool s
    8.68  (* Generalized first-order terms, which include file names, numbers, etc. *)
    8.69 -fun parse_term x =
    8.70 +(* The "x" argument is not strictly necessary, but without it Poly/ML loops
    8.71 +   forever at compile time. *)
    8.72 +fun parse_term pool x =
    8.73    (parse_quoted >> atom
    8.74     || parse_integer >> SInt
    8.75 -   || $$ "$" |-- Symbol.scan_id >> (atom o fix_bool_literal)
    8.76 -   || (Symbol.scan_id >> fix_symbol)
    8.77 -      -- Scan.optional ($$ "(" |-- parse_terms --| $$ ")") [] >> SBranch
    8.78 -   || $$ "(" |-- parse_term --| $$ ")"
    8.79 -   || $$ "[" |-- Scan.optional parse_terms [] --| $$ "]" >> slist_of) x
    8.80 -and parse_terms x = (parse_term ::: Scan.repeat ($$ "," |-- parse_term)) x
    8.81 +   || $$ "$" |-- Symbol.scan_id >> (atom o repair_bool_literal)
    8.82 +   || (Symbol.scan_id >> repair_name pool)
    8.83 +      -- Scan.optional ($$ "(" |-- parse_terms pool --| $$ ")") [] >> SBranch
    8.84 +   || $$ "(" |-- parse_term pool --| $$ ")"
    8.85 +   || $$ "[" |-- Scan.optional (parse_terms pool) [] --| $$ "]" >> slist_of) x
    8.86 +and parse_terms pool x =
    8.87 +  (parse_term pool ::: Scan.repeat ($$ "," |-- parse_term pool)) x
    8.88  
    8.89  fun negate_stree t = SBranch ("c_Not", [t])
    8.90  fun equate_strees t1 t2 = SBranch ("c_equal", [t1, t2]);
    8.91  
    8.92  (* Apply equal or not-equal to a term. *)
    8.93 -fun do_equal (t, NONE) = t
    8.94 -  | do_equal (t1, SOME (NONE, t2)) = equate_strees t1 t2
    8.95 -  | do_equal (t1, SOME (SOME _, t2)) = negate_stree (equate_strees t1 t2)
    8.96 +fun repair_predicate_term (t, NONE) = t
    8.97 +  | repair_predicate_term (t1, SOME (NONE, t2)) = equate_strees t1 t2
    8.98 +  | repair_predicate_term (t1, SOME (SOME _, t2)) =
    8.99 +    negate_stree (equate_strees t1 t2)
   8.100 +fun parse_predicate_term pool =
   8.101 +  parse_term pool -- Scan.option (Scan.option ($$ "!") --| $$ "="
   8.102 +                                  -- parse_term pool)
   8.103 +  >> repair_predicate_term
   8.104  (*Literals can involve negation, = and !=.*)
   8.105 -fun parse_literal x =
   8.106 -  ($$ "~" |-- parse_literal >> negate_stree
   8.107 -   || (parse_term -- Scan.option (Scan.option ($$ "!") --| $$ "=" -- parse_term)
   8.108 -       >> do_equal)) x
   8.109 +fun parse_literal pool x =
   8.110 +  ($$ "~" |-- parse_literal pool >> negate_stree || parse_predicate_term pool) x
   8.111  
   8.112 -val parse_literals = parse_literal ::: Scan.repeat ($$ "|" |-- parse_literal)
   8.113 +fun parse_literals pool =
   8.114 +  parse_literal pool ::: Scan.repeat ($$ "|" |-- parse_literal pool)
   8.115  
   8.116  (*Clause: a list of literals separated by the disjunction sign*)
   8.117 -val parse_clause =
   8.118 -  $$ "(" |-- parse_literals --| $$ ")" || Scan.single parse_literal
   8.119 +fun parse_clause pool =
   8.120 +  $$ "(" |-- parse_literals pool --| $$ ")" || Scan.single (parse_literal pool)
   8.121  
   8.122  fun ints_of_stree (SInt n) = cons n
   8.123    | ints_of_stree (SBranch (_, ts)) = fold ints_of_stree ts
   8.124  val parse_tstp_annotations =
   8.125 -  Scan.optional ($$ "," |-- parse_term --| Scan.option ($$ "," |-- parse_terms)
   8.126 +  Scan.optional ($$ "," |-- parse_term NONE
   8.127 +                   --| Scan.option ($$ "," |-- parse_terms NONE)
   8.128                   >> (fn source => ints_of_stree source [])) []
   8.129  
   8.130  (* <cnf_annotated> ::= cnf(<name>, <formula_role>, <cnf_formula> <annotations>).
   8.131     The <name> could be an identifier, but we assume integers. *)
   8.132  fun retuple_tstp_line ((name, ts), deps) = (name, ts, deps)
   8.133 -val parse_tstp_line =
   8.134 +fun parse_tstp_line pool =
   8.135    (Scan.this_string "cnf" -- $$ "(") |-- parse_integer --| $$ ","
   8.136 -   --| Symbol.scan_id --| $$ "," -- parse_clause -- parse_tstp_annotations
   8.137 +   --| Symbol.scan_id --| $$ "," -- parse_clause pool -- parse_tstp_annotations
   8.138     --| $$ ")" --| $$ "."
   8.139    >> retuple_tstp_line
   8.140  
   8.141 @@ -127,23 +141,26 @@
   8.142  
   8.143  (* It is not clear why some literals are followed by sequences of stars. We
   8.144     ignore them. *)
   8.145 -val parse_starred_literal = parse_literal --| Scan.repeat ($$ "*" || $$ " ")
   8.146 +fun parse_starred_predicate_term pool =
   8.147 +  parse_predicate_term pool --| Scan.repeat ($$ "*" || $$ " ")
   8.148  
   8.149 -val parse_horn_clause =
   8.150 -  Scan.repeat parse_starred_literal --| $$ "-" --| $$ ">"
   8.151 -  -- Scan.repeat parse_starred_literal
   8.152 +fun parse_horn_clause pool =
   8.153 +  Scan.repeat (parse_starred_predicate_term pool) --| $$ "-" --| $$ ">"
   8.154 +  -- Scan.repeat (parse_starred_predicate_term pool)
   8.155    >> (fn ([], []) => [atom "c_False"]
   8.156         | (clauses1, clauses2) => map negate_stree clauses1 @ clauses2)
   8.157  
   8.158 -(* Syntax: <name>[0:<inference><annotations>] || -> <cnf_formula>. *)
   8.159 +(* Syntax: <name>[0:<inference><annotations>] ||
   8.160 +           <cnf_formulas> -> <cnf_formulas>. *)
   8.161  fun retuple_spass_proof_line ((name, deps), ts) = (name, ts, deps)
   8.162 -val parse_spass_proof_line =
   8.163 +fun parse_spass_proof_line pool =
   8.164    parse_integer --| $$ "[" --| $$ "0" --| $$ ":" --| Symbol.scan_id
   8.165    -- parse_spass_annotations --| $$ "]" --| $$ "|" --| $$ "|"
   8.166 -  -- parse_horn_clause --| $$ "."
   8.167 +  -- parse_horn_clause pool --| $$ "."
   8.168    >> retuple_spass_proof_line
   8.169  
   8.170 -val parse_proof_line = fst o (parse_tstp_line || parse_spass_proof_line)
   8.171 +fun parse_proof_line pool = 
   8.172 +  fst o (parse_tstp_line pool || parse_spass_proof_line pool)
   8.173  
   8.174  (**** INTERPRETATION OF TSTP SYNTAX TREES ****)
   8.175  
   8.176 @@ -271,7 +288,7 @@
   8.177        lits_of_strees ctxt (vt, term_of_stree [] (ProofContext.theory_of ctxt) t :: lits) ts;
   8.178  
   8.179  (*Update TVars/TFrees with detected sort constraints.*)
   8.180 -fun fix_sorts vt =
   8.181 +fun repair_sorts vt =
   8.182    let fun tysubst (Type (a, Ts)) = Type (a, map tysubst Ts)
   8.183          | tysubst (TVar (xi, s)) = TVar (xi, the_default s (Vartab.lookup vt xi))
   8.184          | tysubst (TFree (x, s)) = TFree (x, the_default s (Vartab.lookup vt (x, ~1)))
   8.185 @@ -285,9 +302,10 @@
   8.186  
   8.187  (*Interpret a list of syntax trees as a clause, given by "real" literals and sort constraints.
   8.188    vt0 holds the initial sort constraints, from the conjecture clauses.*)
   8.189 -fun clause_of_strees ctxt vt0 ts =
   8.190 -  let val (vt, dt) = lits_of_strees ctxt (vt0,[]) ts in
   8.191 -    singleton (Syntax.check_terms ctxt) (TypeInfer.constrain HOLogic.boolT (fix_sorts vt dt))
   8.192 +fun clause_of_strees ctxt vt ts =
   8.193 +  let val (vt, dt) = lits_of_strees ctxt (vt, []) ts in
   8.194 +    dt |> repair_sorts vt |> TypeInfer.constrain HOLogic.boolT
   8.195 +       |> Syntax.check_term ctxt
   8.196    end
   8.197  
   8.198  fun gen_all_vars t = fold_rev Logic.all (OldTerm.term_vars t) t;
   8.199 @@ -491,10 +509,10 @@
   8.200  fun isar_proof_end 1 = "qed"
   8.201    | isar_proof_end _ = "next"
   8.202  
   8.203 -fun isar_proof_from_atp_proof cnfs modulus sorts ctxt goal i thm_names =
   8.204 +fun isar_proof_from_atp_proof pool modulus sorts ctxt cnfs thm_names goal i =
   8.205    let
   8.206      val _ = trace_proof_msg (K "\nisar_proof_from_atp_proof: start\n")
   8.207 -    val tuples = map (parse_proof_line o explode) cnfs
   8.208 +    val tuples = map (parse_proof_line pool o explode) cnfs
   8.209      val _ = trace_proof_msg (fn () =>
   8.210        Int.toString (length tuples) ^ " tuples extracted\n")
   8.211      val ctxt = ProofContext.set_mode ProofContext.mode_schematic ctxt
   8.212 @@ -600,7 +618,7 @@
   8.213  
   8.214  val strip_spaces = strip_spaces_in_list o String.explode
   8.215  
   8.216 -fun isar_proof_text debug modulus sorts ctxt
   8.217 +fun isar_proof_text pool debug modulus sorts ctxt
   8.218                      (minimize_command, proof, thm_names, goal, i) =
   8.219    let
   8.220      val cnfs = proof |> split_lines |> map strip_spaces |> filter is_proof_line
   8.221 @@ -608,7 +626,8 @@
   8.222        metis_proof_text (minimize_command, proof, thm_names, goal, i)
   8.223      val tokens = String.tokens (fn c => c = #" ") one_line_proof
   8.224      fun isar_proof_for () =
   8.225 -      case isar_proof_from_atp_proof cnfs modulus sorts ctxt goal i thm_names of
   8.226 +      case isar_proof_from_atp_proof pool modulus sorts ctxt cnfs thm_names goal
   8.227 +                                     i of
   8.228          "" => ""
   8.229        | isar_proof =>
   8.230          "\nStructured proof:\n" ^ Markup.markup Markup.sendback isar_proof
   8.231 @@ -622,8 +641,8 @@
   8.232          |> the_default "Warning: The Isar proof construction failed.\n"
   8.233    in (one_line_proof ^ isar_proof, lemma_names) end
   8.234  
   8.235 -fun proof_text isar_proof debug modulus sorts ctxt =
   8.236 -  if isar_proof then isar_proof_text debug modulus sorts ctxt
   8.237 +fun proof_text isar_proof pool debug modulus sorts ctxt =
   8.238 +  if isar_proof then isar_proof_text pool debug modulus sorts ctxt
   8.239    else metis_proof_text
   8.240  
   8.241  end;