generate full first-order formulas (FOF) in Sledgehammer
authorblanchet
Mon Jul 26 17:03:21 2010 +0200 (2010-07-26)
changeset 3799506f02b15ef8a
parent 37994 b04307085a09
child 37996 11c076ea92e9
generate full first-order formulas (FOF) in Sledgehammer
src/HOL/Tools/ATP_Manager/atp_systems.ML
src/HOL/Tools/Sledgehammer/clausifier.ML
src/HOL/Tools/Sledgehammer/metis_clauses.ML
src/HOL/Tools/Sledgehammer/sledgehammer_fact_filter.ML
src/HOL/Tools/Sledgehammer/sledgehammer_proof_reconstruct.ML
src/HOL/Tools/Sledgehammer/sledgehammer_tptp_format.ML
src/HOL/Tools/Sledgehammer/sledgehammer_util.ML
     1.1 --- a/src/HOL/Tools/ATP_Manager/atp_systems.ML	Mon Jul 26 14:14:24 2010 +0200
     1.2 +++ b/src/HOL/Tools/ATP_Manager/atp_systems.ML	Mon Jul 26 17:03:21 2010 +0200
     1.3 @@ -115,13 +115,6 @@
     1.4    | string_for_failure MalformedOutput = "Error: The ATP output is malformed."
     1.5    | string_for_failure UnknownError = "Error: An unknown ATP error occurred."
     1.6  
     1.7 -fun shape_of_clauses _ [] = []
     1.8 -  | shape_of_clauses j ([] :: clauses) = [] :: shape_of_clauses j clauses
     1.9 -  | shape_of_clauses j ((_ :: lits) :: clauses) =
    1.10 -    let val shape = shape_of_clauses (j + 1) (lits :: clauses) in
    1.11 -      (j :: hd shape) :: tl shape
    1.12 -    end
    1.13 -
    1.14  
    1.15  (* Clause preparation *)
    1.16  
    1.17 @@ -133,24 +126,42 @@
    1.18  fun subtract_cls ax_clauses =
    1.19    filter_out (Termtab.defined (make_clause_table ax_clauses) o prop_of)
    1.20  
    1.21 -(* FIXME: kill *)
    1.22 -fun mk_anot phi = AConn (ANot, [phi])
    1.23 -fun mk_aconn c phi1 phi2 = AConn (c, [phi1, phi2])
    1.24 +fun combformula_for_prop thy =
    1.25 +  let
    1.26 +    val do_term = combterm_from_term thy
    1.27 +    fun do_quant bs q s T t' =
    1.28 +      do_formula ((s, T) :: bs) t'
    1.29 +      #>> (fn phi => AQuant (q, [`make_bound_var s], phi))
    1.30 +    and do_conn bs c t1 t2 =
    1.31 +      do_formula bs t1 ##>> do_formula bs t2
    1.32 +      #>> (fn (phi1, phi2) => AConn (c, [phi1, phi2]))
    1.33 +    and do_formula bs t =
    1.34 +      case t of
    1.35 +        @{const Trueprop} $ t1 => do_formula bs t1
    1.36 +      | @{const Not} $ t1 =>
    1.37 +        do_formula bs t1 #>> (fn phi => AConn (ANot, [phi]))
    1.38 +      | Const (@{const_name All}, _) $ Abs (s, T, t') =>
    1.39 +        do_quant bs AForall s T t'
    1.40 +      | Const (@{const_name Ex}, _) $ Abs (s, T, t') =>
    1.41 +        do_quant bs AExists s T t'
    1.42 +      | @{const "op &"} $ t1 $ t2 => do_conn bs AAnd t1 t2
    1.43 +      | @{const "op |"} $ t1 $ t2 => do_conn bs AOr t1 t2
    1.44 +      | @{const "op -->"} $ t1 $ t2 => do_conn bs AImplies t1 t2
    1.45 +      | Const (@{const_name "op ="}, Type (_, [@{typ bool}, _])) $ t1 $ t2 =>
    1.46 +        do_conn bs AIff t1 t2
    1.47 +      | _ => (fn ts => do_term bs (Envir.eta_contract t)
    1.48 +                       |>> APred ||> union (op =) ts)
    1.49 +  in do_formula [] end
    1.50  
    1.51  (* making axiom and conjecture clauses *)
    1.52 -fun make_clause thy (formula_id, formula_name, kind, th) skolems =
    1.53 +fun make_clause thy (formula_id, formula_name, kind, t) skolems =
    1.54    let
    1.55 -    val (skolems, t) = th |> prop_of |> conceal_skolem_terms formula_id skolems
    1.56 -    val (lits, ctypes_sorts) = literals_of_term thy t
    1.57 -    (* FIXME: avoid "literals_of_term *)
    1.58 -    val combformula =
    1.59 -      case lits of
    1.60 -        [] => APred (CombConst (("c_False", "False"), CombType (("bool", "bool"), []), []))
    1.61 -      | _ =>
    1.62 -        let val phis = lits |> map (fn FOLLiteral (pos, tm) => APred tm |> not pos ? mk_anot) in
    1.63 -          fold (mk_aconn AOr) (tl phis) (hd phis)
    1.64 -          |> kind = Conjecture ? mk_anot
    1.65 -        end
    1.66 +    (* ### FIXME: introduce combinators and perform other transformations
    1.67 +       previously done by Clausifier.to_nnf *)
    1.68 +    val (skolems, t) =
    1.69 +      t |> Object_Logic.atomize_term thy
    1.70 +        |> conceal_skolem_terms formula_id skolems
    1.71 +    val (combformula, ctypes_sorts) = combformula_for_prop thy t []
    1.72    in
    1.73      (skolems,
    1.74       FOLFormula {formula_name = formula_name, formula_id = formula_id,
    1.75 @@ -160,7 +171,7 @@
    1.76  
    1.77  fun add_axiom_clause thy ((name, k), th) (skolems, clss) =
    1.78    let
    1.79 -    val (skolems, cls) = make_clause thy (k, name, Axiom, th) skolems
    1.80 +    val (skolems, cls) = make_clause thy (k, name, Axiom, prop_of th) skolems
    1.81    in (skolems, (name, cls) :: clss) end
    1.82  
    1.83  fun make_axiom_clauses thy clauses =
    1.84 @@ -169,11 +180,11 @@
    1.85  fun make_conjecture_clauses thy =
    1.86    let
    1.87      fun aux _ _ [] = []
    1.88 -      | aux n skolems (th :: ths) =
    1.89 +      | aux n skolems (t :: ts) =
    1.90          let
    1.91            val (skolems, cls) =
    1.92 -            make_clause thy (n, "conjecture", Conjecture, th) skolems
    1.93 -        in cls :: aux (n + 1) skolems ths end
    1.94 +            make_clause thy (n, "conjecture", Conjecture, t) skolems
    1.95 +        in cls :: aux (n + 1) skolems ts end
    1.96    in aux 0 [] end
    1.97  
    1.98  (** Helper clauses **)
    1.99 @@ -220,20 +231,24 @@
   1.100        @ (if is_FO then [] else cnf_helper_thms thy false mandatory_helpers)
   1.101    in map snd (make_axiom_clauses thy cnfs) end
   1.102  
   1.103 +fun negate_prop (@{const Trueprop} $ t) = negate_prop t
   1.104 +  | negate_prop (@{const Not} $ t) = t
   1.105 +  | negate_prop t = @{const Not} $ t
   1.106 +
   1.107  (* prepare for passing to writer,
   1.108     create additional clauses based on the information from extra_cls *)
   1.109 -fun prepare_clauses full_types goal_cls axcls extra_cls thy =
   1.110 +fun prepare_clauses full_types hyp_ts concl_t axcls extra_cls thy =
   1.111    let
   1.112 -    val is_FO = forall (Meson.is_fol_term thy o prop_of) goal_cls
   1.113 -    val ccls = subtract_cls extra_cls goal_cls
   1.114 -    val _ = app (fn th => trace_msg (fn _ => Display.string_of_thm_global thy th)) ccls
   1.115 -    val ccltms = map prop_of ccls
   1.116 -    and axtms = map (prop_of o snd) extra_cls
   1.117 -    val subs = tfree_classes_of_terms ccltms
   1.118 -    and supers = tvar_classes_of_terms axtms
   1.119 -    and tycons = type_consts_of_terms thy (ccltms @ axtms)
   1.120 +    val goal_t = Logic.list_implies (hyp_ts, concl_t)
   1.121 +    val is_FO = Meson.is_fol_term thy goal_t
   1.122 +    val _ = trace_msg (fn _ => Syntax.string_of_term_global thy goal_t)
   1.123 +    val axtms = map (prop_of o snd) extra_cls
   1.124 +    val subs = tfree_classes_of_terms [goal_t]
   1.125 +    val supers = tvar_classes_of_terms axtms
   1.126 +    val tycons = type_consts_of_terms thy (goal_t :: axtms)
   1.127      (*TFrees in conjecture clauses; TVars in axiom clauses*)
   1.128 -    val conjectures = make_conjecture_clauses thy ccls
   1.129 +    val conjectures =
   1.130 +      make_conjecture_clauses thy (map negate_prop hyp_ts @ [concl_t])
   1.131      val (_, extra_clauses) = ListPair.unzip (make_axiom_clauses thy extra_cls)
   1.132      val (clnames, axiom_clauses) = ListPair.unzip (make_axiom_clauses thy axcls)
   1.133      val helper_clauses =
   1.134 @@ -307,20 +322,20 @@
   1.135      (* get clauses and prepare them for writing *)
   1.136      val (ctxt, (_, th)) = goal;
   1.137      val thy = ProofContext.theory_of ctxt;
   1.138 -    val goal_clss = #1 (Clausifier.neg_conjecture_clauses ctxt th subgoal)
   1.139 -    val goal_cls = List.concat goal_clss
   1.140 +    (* ### FIXME: (1) preprocessing for "if" etc. *)
   1.141 +    val (params, hyp_ts, concl_t) = strip_subgoal th subgoal
   1.142      val the_filtered_clauses =
   1.143        case filtered_clauses of
   1.144          SOME fcls => fcls
   1.145        | NONE => relevant_facts full_types relevance_threshold
   1.146                      relevance_convergence defs_relevant max_axiom_clauses
   1.147                      (the_default prefers_theory_relevant theory_relevant)
   1.148 -                    relevance_override goal goal_cls
   1.149 +                    relevance_override goal hyp_ts concl_t
   1.150                  |> Clausifier.cnf_rules_pairs thy true
   1.151      val the_axiom_clauses = axiom_clauses |> the_default the_filtered_clauses
   1.152      val (internal_thm_names, clauses) =
   1.153 -      prepare_clauses full_types goal_cls the_axiom_clauses the_filtered_clauses
   1.154 -                      thy
   1.155 +      prepare_clauses full_types hyp_ts concl_t the_axiom_clauses
   1.156 +                      the_filtered_clauses thy
   1.157  
   1.158      (* path to unique problem file *)
   1.159      val the_dest_dir = if overlord then getenv "ISABELLE_HOME_USER"
   1.160 @@ -387,7 +402,9 @@
   1.161            val (pool, conjecture_offset) =
   1.162              write_tptp_file thy readable_names explicit_forall full_types
   1.163                              explicit_apply probfile clauses
   1.164 -          val conjecture_shape = shape_of_clauses (conjecture_offset + 1) goal_clss
   1.165 +          val conjecture_shape =
   1.166 +            conjecture_offset + 1 upto conjecture_offset + length hyp_ts + 1
   1.167 +            |> map single (* ### FIXME: get rid of "map single" *)
   1.168            val result =
   1.169              do_run false
   1.170              |> (fn (_, msecs0, _, SOME _) =>
   1.171 @@ -448,8 +465,8 @@
   1.172       string_of_int (to_generous_secs timeout),
   1.173     proof_delims = [tstp_proof_delims],
   1.174     known_failures =
   1.175 -     [(Unprovable, "SZS status: Satisfiable"),
   1.176 -      (Unprovable, "SZS status Satisfiable"),
   1.177 +     [(Unprovable, "SZS status: CounterSatisfiable"),
   1.178 +      (Unprovable, "SZS status CounterSatisfiable"),
   1.179        (TimedOut, "Failure: Resource limit exceeded (time)"),
   1.180        (TimedOut, "time limit exceeded"),
   1.181        (OutOfResources,
     2.1 --- a/src/HOL/Tools/Sledgehammer/clausifier.ML	Mon Jul 26 14:14:24 2010 +0200
     2.2 +++ b/src/HOL/Tools/Sledgehammer/clausifier.ML	Mon Jul 26 17:03:21 2010 +0200
     2.3 @@ -11,8 +11,6 @@
     2.4    val cnf_rules_pairs :
     2.5      theory -> bool -> (string * thm) list -> ((string * int) * thm) list
     2.6    val neg_clausify: thm -> thm list
     2.7 -  val neg_conjecture_clauses:
     2.8 -    Proof.context -> thm -> int -> thm list list * (string * typ) list
     2.9  end;
    2.10  
    2.11  structure Clausifier : CLAUSIFIER =
    2.12 @@ -222,7 +220,8 @@
    2.13      |> Thm.varifyT_global
    2.14    end
    2.15  
    2.16 -(*Converts an Isabelle theorem (intro, elim or simp format, even higher-order) into NNF.*)
    2.17 +(* Converts an Isabelle theorem (intro, elim or simp format, even higher-order)
    2.18 +   into NNF. *)
    2.19  fun to_nnf th ctxt0 =
    2.20    let val th1 = th |> transform_elim |> zero_var_indexes
    2.21        val ((_, [th2]), ctxt) = Variable.import true [th1] ctxt0
    2.22 @@ -231,7 +230,7 @@
    2.23                      |> Meson.make_nnf ctxt
    2.24    in  (th3, ctxt)  end;
    2.25  
    2.26 -(*Skolemize a named theorem, with Skolem functions as additional premises.*)
    2.27 +(* Skolemize a named theorem, with Skolem functions as additional premises. *)
    2.28  fun skolemize_theorem thy cheat th =
    2.29    let
    2.30      val ctxt0 = Variable.global_thm_context th
    2.31 @@ -255,6 +254,7 @@
    2.32  (**** Translate a set of theorems into CNF ****)
    2.33  
    2.34  (*The combination of rev and tail recursion preserves the original order*)
    2.35 +(* ### FIXME: kill "cheat" *)
    2.36  fun cnf_rules_pairs thy cheat =
    2.37    let
    2.38      fun do_one _ [] = []
    2.39 @@ -280,13 +280,4 @@
    2.40    #> map introduce_combinators
    2.41    #> Meson.finish_cnf
    2.42  
    2.43 -fun neg_conjecture_clauses ctxt st0 n =
    2.44 -  let
    2.45 -    (* "Option" is thrown if the assumptions contain schematic variables. *)
    2.46 -    val st = Seq.hd (neg_skolemize_tac ctxt n st0) handle Option.Option => st0
    2.47 -    val ({params, prems, ...}, _) =
    2.48 -      Subgoal.focus (Variable.set_body false ctxt) n st
    2.49 -  in (map neg_clausify prems, map (dest_Free o term_of o #2) params) end
    2.50 -
    2.51 -
    2.52  end;
     3.1 --- a/src/HOL/Tools/Sledgehammer/metis_clauses.ML	Mon Jul 26 14:14:24 2010 +0200
     3.2 +++ b/src/HOL/Tools/Sledgehammer/metis_clauses.ML	Mon Jul 26 17:03:21 2010 +0200
     3.3 @@ -34,6 +34,7 @@
     3.4                    literals: fol_literal list, ctypes_sorts: typ list}
     3.5  
     3.6    val type_wrapper_name : string
     3.7 +  val bound_var_prefix : string
     3.8    val schematic_var_prefix: string
     3.9    val fixed_var_prefix: string
    3.10    val tvar_prefix: string
    3.11 @@ -46,6 +47,7 @@
    3.12    val ascii_of: string -> string
    3.13    val undo_ascii_of: string -> string
    3.14    val strip_prefix_and_undo_ascii: string -> string -> string option
    3.15 +  val make_bound_var : string -> string
    3.16    val make_schematic_var : string * int -> string
    3.17    val make_fixed_var : string -> string
    3.18    val make_schematic_type_var : string * int -> string
    3.19 @@ -63,6 +65,8 @@
    3.20    val make_arity_clauses: theory -> string list -> class list -> class list * arity_clause list
    3.21    val combtyp_of : combterm -> combtyp
    3.22    val strip_combterm_comb : combterm -> combterm * combterm list
    3.23 +  val combterm_from_term :
    3.24 +    theory -> (string * typ) list -> term -> combterm * typ list
    3.25    val literals_of_term : theory -> term -> fol_literal list * typ list
    3.26    val conceal_skolem_terms :
    3.27      int -> (string * term) list -> term -> (string * term) list * term
    3.28 @@ -77,8 +81,9 @@
    3.29  
    3.30  val type_wrapper_name = "ti"
    3.31  
    3.32 -val schematic_var_prefix = "V_";
    3.33 -val fixed_var_prefix = "v_";
    3.34 +val bound_var_prefix = "B_"
    3.35 +val schematic_var_prefix = "V_"
    3.36 +val fixed_var_prefix = "v_"
    3.37  
    3.38  val tvar_prefix = "T_";
    3.39  val tfree_prefix = "t_";
    3.40 @@ -177,8 +182,9 @@
    3.41  fun ascii_of_indexname (v,0) = ascii_of v
    3.42    | ascii_of_indexname (v,i) = ascii_of v ^ "_" ^ Int.toString i;
    3.43  
    3.44 -fun make_schematic_var v = schematic_var_prefix ^ (ascii_of_indexname v);
    3.45 -fun make_fixed_var x = fixed_var_prefix ^ (ascii_of x);
    3.46 +fun make_bound_var x = bound_var_prefix ^ ascii_of x
    3.47 +fun make_schematic_var v = schematic_var_prefix ^ ascii_of_indexname v
    3.48 +fun make_fixed_var x = fixed_var_prefix ^ ascii_of x
    3.49  
    3.50  fun make_schematic_type_var (x,i) =
    3.51        tvar_prefix ^ (ascii_of_indexname (trim_type_var x,i));
    3.52 @@ -402,8 +408,13 @@
    3.53    | simp_type_of (TVar (x, _)) =
    3.54      CombTVar (make_schematic_type_var x, string_of_indexname x)
    3.55  
    3.56 -(* convert a Term.term (with combinators) into a combterm, also accummulate sort info *)
    3.57 -fun combterm_of thy (Const (c, T)) =
    3.58 +(* Converts a term (with combinators) into a combterm. Also accummulates sort
    3.59 +   infomation. *)
    3.60 +fun combterm_from_term thy bs (P $ Q) =
    3.61 +      let val (P', tsP) = combterm_from_term thy bs P
    3.62 +          val (Q', tsQ) = combterm_from_term thy bs Q
    3.63 +      in  (CombApp (P', Q'), union (op =) tsP tsQ)  end
    3.64 +  | combterm_from_term thy _ (Const (c, T)) =
    3.65        let
    3.66          val (tp, ts) = type_of T
    3.67          val tvar_list =
    3.68 @@ -414,22 +425,25 @@
    3.69            |> map simp_type_of
    3.70          val c' = CombConst (`make_fixed_const c, tp, tvar_list)
    3.71        in  (c',ts)  end
    3.72 -  | combterm_of _ (Free(v, T)) =
    3.73 +  | combterm_from_term _ _ (Free (v, T)) =
    3.74        let val (tp,ts) = type_of T
    3.75            val v' = CombConst (`make_fixed_var v, tp, [])
    3.76        in  (v',ts)  end
    3.77 -  | combterm_of _ (Var(v, T)) =
    3.78 +  | combterm_from_term _ _ (Var (v, T)) =
    3.79        let val (tp,ts) = type_of T
    3.80            val v' = CombVar ((make_schematic_var v, string_of_indexname v), tp)
    3.81        in  (v',ts)  end
    3.82 -  | combterm_of thy (P $ Q) =
    3.83 -      let val (P', tsP) = combterm_of thy P
    3.84 -          val (Q', tsQ) = combterm_of thy Q
    3.85 -      in  (CombApp (P', Q'), union (op =) tsP tsQ)  end
    3.86 -  | combterm_of _ (Abs _) = raise Fail "HOL clause: Abs"
    3.87 +  | combterm_from_term _ bs (Bound j) =
    3.88 +      let
    3.89 +        val (s, T) = nth bs j
    3.90 +        val (tp, ts) = type_of T
    3.91 +        val v' = CombConst (`make_bound_var s, tp, [])
    3.92 +      in (v', ts) end
    3.93 +  | combterm_from_term _ _ (Abs _) = raise Fail "HOL clause: Abs"
    3.94  
    3.95  fun predicate_of thy ((@{const Not} $ P), pos) = predicate_of thy (P, not pos)
    3.96 -  | predicate_of thy (t, pos) = (combterm_of thy (Envir.eta_contract t), pos)
    3.97 +  | predicate_of thy (t, pos) =
    3.98 +    (combterm_from_term thy [] (Envir.eta_contract t), pos)
    3.99  
   3.100  fun literals_of_term1 args thy (@{const Trueprop} $ P) =
   3.101      literals_of_term1 args thy P
     4.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_fact_filter.ML	Mon Jul 26 14:14:24 2010 +0200
     4.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_fact_filter.ML	Mon Jul 26 17:03:21 2010 +0200
     4.3 @@ -16,7 +16,8 @@
     4.4      Proof.context -> thm list -> Facts.ref -> string * thm list
     4.5    val relevant_facts :
     4.6      bool -> real -> real -> bool -> int -> bool -> relevance_override
     4.7 -    -> Proof.context * (thm list * 'a) -> thm list -> (string * thm) list
     4.8 +    -> Proof.context * (thm list * 'a) -> term list -> term
     4.9 +    -> (string * thm) list
    4.10  end;
    4.11  
    4.12  structure Sledgehammer_Fact_Filter : SLEDGEHAMMER_FACT_FILTER =
    4.13 @@ -148,9 +149,8 @@
    4.14          do_term t0 #> do_formula pos t1  (* theory constant *)
    4.15        | _ => do_term t
    4.16    in
    4.17 -    Symtab.empty
    4.18 -    |> fold (Symtab.update o rpair []) boring_natural_consts
    4.19 -    |> fold (do_formula pos) ts
    4.20 +    Symtab.empty |> fold (Symtab.update o rpair []) boring_natural_consts
    4.21 +                 |> fold (do_formula pos) ts
    4.22    end
    4.23  
    4.24  (*Inserts a dummy "constant" referring to the theory name, so that relevance
    4.25 @@ -343,7 +343,7 @@
    4.26  
    4.27  fun relevance_filter ctxt relevance_threshold relevance_convergence
    4.28                       defs_relevant max_new theory_relevant relevance_override
    4.29 -                     thy axioms goals =
    4.30 +                     thy axioms goal_ts =
    4.31    if relevance_threshold > 1.0 then
    4.32      []
    4.33    else if relevance_threshold < 0.0 then
    4.34 @@ -352,7 +352,7 @@
    4.35      let
    4.36        val const_tab = fold (count_axiom_consts theory_relevant thy) axioms
    4.37                             Symtab.empty
    4.38 -      val goal_const_tab = get_consts_typs thy (SOME true) goals
    4.39 +      val goal_const_tab = get_consts_typs thy (SOME true) goal_ts
    4.40        val relevance_threshold = 0.9 * relevance_threshold (* FIXME *)
    4.41        val _ =
    4.42          trace_msg (fn () => "Initial constants: " ^
    4.43 @@ -563,12 +563,14 @@
    4.44  fun relevant_facts full_types relevance_threshold relevance_convergence
    4.45                     defs_relevant max_new theory_relevant
    4.46                     (relevance_override as {add, del, only})
    4.47 -                   (ctxt, (chained_ths, _)) goal_cls =
    4.48 +                   (ctxt, (chained_ths, _)) hyp_ts concl_t =
    4.49    let
    4.50      val thy = ProofContext.theory_of ctxt
    4.51      val add_thms = maps (ProofContext.get_fact ctxt) add
    4.52      val has_override = not (null add) orelse not (null del)
    4.53 -    val is_FO = forall (Meson.is_fol_term thy o prop_of) goal_cls
    4.54 +(*###
    4.55 +    val is_FO = forall Meson.is_fol_term thy (concl_t :: hyp_ts)
    4.56 +*)
    4.57      val axioms =
    4.58        checked_name_thm_pairs (respect_no_atp andalso not only) ctxt
    4.59            (map (name_thms_pair_from_ref ctxt chained_ths) add @
    4.60 @@ -581,7 +583,7 @@
    4.61    in
    4.62      relevance_filter ctxt relevance_threshold relevance_convergence
    4.63                       defs_relevant max_new theory_relevant relevance_override
    4.64 -                     thy axioms (map prop_of goal_cls)
    4.65 +                     thy axioms (concl_t :: hyp_ts)
    4.66      |> has_override ? make_unique
    4.67      |> sort_wrt fst
    4.68    end
     5.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_proof_reconstruct.ML	Mon Jul 26 14:14:24 2010 +0200
     5.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_proof_reconstruct.ML	Mon Jul 26 17:03:21 2010 +0200
     5.3 @@ -954,17 +954,12 @@
     5.4          do_indent 0 ^ (if n <> 1 then "next" else "qed") ^ "\n"
     5.5    in do_proof end
     5.6  
     5.7 -fun strip_subgoal goal i =
     5.8 -  let
     5.9 -    val (t, frees) = Logic.goal_params (prop_of goal) i
    5.10 -    val hyp_ts = t |> Logic.strip_assums_hyp |> map (curry subst_bounds frees)
    5.11 -    val concl_t = t |> Logic.strip_assums_concl |> curry subst_bounds frees
    5.12 -  in (rev (map dest_Free frees), hyp_ts, concl_t) end
    5.13 -
    5.14  fun isar_proof_text (pool, debug, isar_shrink_factor, ctxt, conjecture_shape)
    5.15                      (other_params as (full_types, _, atp_proof, thm_names, goal,
    5.16                                        i)) =
    5.17    let
    5.18 +    (* ### FIXME: avoid duplication with ATP_Systems -- and move strip_subgoal
    5.19 +       to ATP_Systems *)
    5.20      val (params, hyp_ts, concl_t) = strip_subgoal goal i
    5.21      val frees = fold Term.add_frees (concl_t :: hyp_ts) []
    5.22      val tfrees = fold Term.add_tfrees (concl_t :: hyp_ts) []
     6.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_tptp_format.ML	Mon Jul 26 14:14:24 2010 +0200
     6.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_tptp_format.ML	Mon Jul 26 17:03:21 2010 +0200
     6.3 @@ -76,7 +76,7 @@
     6.4    | string_for_connective AIff = "<=>"
     6.5    | string_for_connective ANotIff = "<~>"
     6.6  fun string_for_formula (AQuant (q, xs, phi)) =
     6.7 -    string_for_quantifier q ^ " [" ^ commas xs ^ "] : " ^
     6.8 +    string_for_quantifier q ^ "[" ^ commas xs ^ "]: " ^
     6.9      string_for_formula phi
    6.10    | string_for_formula (AConn (c, [phi])) =
    6.11      string_for_connective c ^ " " ^ string_for_formula phi
     7.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_util.ML	Mon Jul 26 14:14:24 2010 +0200
     7.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_util.ML	Mon Jul 26 17:03:21 2010 +0200
     7.3 @@ -18,6 +18,7 @@
     7.4    val maybe_quote : string -> string
     7.5    val monomorphic_term : Type.tyenv -> term -> term
     7.6    val specialize_type : theory -> (string * typ) -> term -> term
     7.7 +  val strip_subgoal : thm -> int -> (string * typ) list * term list * term
     7.8  end;
     7.9   
    7.10  structure Sledgehammer_Util : SLEDGEHAMMER_UTIL =
    7.11 @@ -126,5 +127,11 @@
    7.12      | NONE => raise Type.TYPE_MATCH
    7.13    end
    7.14  
    7.15 +fun strip_subgoal goal i =
    7.16 +  let
    7.17 +    val (t, frees) = Logic.goal_params (prop_of goal) i
    7.18 +    val hyp_ts = t |> Logic.strip_assums_hyp |> map (curry subst_bounds frees)
    7.19 +    val concl_t = t |> Logic.strip_assums_concl |> curry subst_bounds frees
    7.20 +  in (rev (map dest_Free frees), hyp_ts, concl_t) end
    7.21  
    7.22  end;