proper polymorphic Skolemization of uncached facts + synchronization of caching and relevance filter
authorblanchet
Fri Jun 11 17:10:23 2010 +0200 (2010-06-11)
changeset 3739934f080a12063
parent 37398 e194213451c9
child 37400 cf5e06d5ecaf
proper polymorphic Skolemization of uncached facts + synchronization of caching and relevance filter
src/HOL/Sledgehammer.thy
src/HOL/Tools/Sledgehammer/metis_tactics.ML
src/HOL/Tools/Sledgehammer/sledgehammer_fact_filter.ML
src/HOL/Tools/Sledgehammer/sledgehammer_fact_preprocessor.ML
src/HOL/Tools/Sledgehammer/sledgehammer_hol_clause.ML
src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML
src/HOL/Tools/Sledgehammer/sledgehammer_proof_reconstruct.ML
     1.1 --- a/src/HOL/Sledgehammer.thy	Fri Jun 11 17:07:27 2010 +0200
     1.2 +++ b/src/HOL/Sledgehammer.thy	Fri Jun 11 17:10:23 2010 +0200
     1.3 @@ -25,6 +25,12 @@
     1.4    ("Tools/Sledgehammer/metis_tactics.ML")
     1.5  begin
     1.6  
     1.7 +definition skolem_Eps :: "('a \<Rightarrow> bool) \<Rightarrow> 'a" where
     1.8 +[no_atp]: "skolem_Eps = Eps"
     1.9 +
    1.10 +lemma skolem_someI_ex [no_atp]: "\<exists>x. P x \<Longrightarrow> P (skolem_Eps (\<lambda>x. P x))"
    1.11 +unfolding skolem_Eps_def by (rule someI_ex)
    1.12 +
    1.13  definition COMBI :: "'a \<Rightarrow> 'a" where
    1.14  [no_atp]: "COMBI P \<equiv> P"
    1.15  
     2.1 --- a/src/HOL/Tools/Sledgehammer/metis_tactics.ML	Fri Jun 11 17:07:27 2010 +0200
     2.2 +++ b/src/HOL/Tools/Sledgehammer/metis_tactics.ML	Fri Jun 11 17:10:23 2010 +0200
     2.3 @@ -18,6 +18,7 @@
     2.4  structure Metis_Tactics : METIS_TACTICS =
     2.5  struct
     2.6  
     2.7 +open Sledgehammer_Util
     2.8  open Sledgehammer_FOL_Clause
     2.9  open Sledgehammer_Fact_Preprocessor
    2.10  open Sledgehammer_HOL_Clause
    2.11 @@ -118,7 +119,7 @@
    2.12              metis_lit pol "=" (map hol_term_to_fol_FT tms)
    2.13          | _ => metis_lit pol "{}" [hol_term_to_fol_FT tm])   (*hBOOL*);
    2.14  
    2.15 -fun literals_of_hol_thm thy mode t =
    2.16 +fun literals_of_hol_term thy mode t =
    2.17        let val (lits, types_sorts) = literals_of_term thy t
    2.18        in  (map (hol_literal_to_fol mode) lits, types_sorts) end;
    2.19  
    2.20 @@ -134,21 +135,24 @@
    2.21  fun metis_of_tfree tf =
    2.22    Metis.Thm.axiom (Metis.LiteralSet.singleton (metis_of_type_literals true tf));
    2.23  
    2.24 -fun hol_thm_to_fol is_conjecture ctxt mode th =
    2.25 -  let val thy = ProofContext.theory_of ctxt
    2.26 -      val (mlits, types_sorts) =
    2.27 -             (literals_of_hol_thm thy mode o HOLogic.dest_Trueprop o prop_of) th
    2.28 +fun hol_thm_to_fol is_conjecture ctxt mode j skolem_somes th =
    2.29 +  let
    2.30 +    val thy = ProofContext.theory_of ctxt
    2.31 +    val (skolem_somes, (mlits, types_sorts)) =
    2.32 +     th |> prop_of |> kill_skolem_Eps j skolem_somes
    2.33 +        ||> (HOLogic.dest_Trueprop #> literals_of_hol_term thy mode)
    2.34    in
    2.35        if is_conjecture then
    2.36            (Metis.Thm.axiom (Metis.LiteralSet.fromList mlits),
    2.37 -           type_literals_for_types types_sorts)
    2.38 +           type_literals_for_types types_sorts, skolem_somes)
    2.39        else
    2.40          let val tylits = filter_out (default_sort ctxt) types_sorts
    2.41                           |> type_literals_for_types
    2.42              val mtylits = if Config.get ctxt type_lits
    2.43                            then map (metis_of_type_literals false) tylits else []
    2.44          in
    2.45 -          (Metis.Thm.axiom (Metis.LiteralSet.fromList(mtylits @ mlits)), [])
    2.46 +          (Metis.Thm.axiom (Metis.LiteralSet.fromList(mtylits @ mlits)), [],
    2.47 +           skolem_somes)
    2.48          end
    2.49    end;
    2.50  
    2.51 @@ -231,10 +235,30 @@
    2.52            SOME tf => mk_tfree ctxt tf
    2.53          | NONE    => error ("fol_type_to_isa: " ^ x));
    2.54  
    2.55 +fun reintroduce_skolem_Eps thy skolem_somes =
    2.56 +  let
    2.57 +    fun aux Ts args t =
    2.58 +      case t of
    2.59 +        t1 $ t2 => aux Ts (aux Ts [] t2 :: args) t1
    2.60 +      | Abs (s, T, t') => list_comb (Abs (s, T, aux (T :: Ts) [] t'), args)
    2.61 +      | Const (s, T) =>
    2.62 +        if String.isPrefix skolem_Eps_pseudo_theory s then
    2.63 +          let
    2.64 +            val (T', args', def') = AList.lookup (op =) skolem_somes s |> the
    2.65 +          in
    2.66 +            def' |> subst_free (args' ~~ args)
    2.67 +                 |> map_types Type_Infer.paramify_vars
    2.68 +          end
    2.69 +        else
    2.70 +          list_comb (t, args)
    2.71 +      | t => list_comb (t, args)
    2.72 +  in aux [] [] end
    2.73 +
    2.74  (*Maps metis terms to isabelle terms*)
    2.75 -fun fol_term_to_hol_RAW ctxt fol_tm =
    2.76 +fun hol_term_from_fol_PT ctxt fol_tm =
    2.77    let val thy = ProofContext.theory_of ctxt
    2.78 -      val _ = trace_msg (fn () => "fol_term_to_hol: " ^ Metis.Term.toString fol_tm)
    2.79 +      val _ = trace_msg (fn () => "hol_term_from_fol_PT: " ^
    2.80 +                                  Metis.Term.toString fol_tm)
    2.81        fun tm_to_tt (Metis.Term.Var v) =
    2.82               (case strip_prefix tvar_prefix v of
    2.83                    SOME w => Type (make_tvar w)
    2.84 @@ -285,11 +309,16 @@
    2.85                    let val opr = Term.Free(b, HOLogic.typeT)
    2.86                    in  apply_list opr (length ts) (map tm_to_tt ts)  end
    2.87                | NONE => error ("unexpected metis function: " ^ a)
    2.88 -  in  case tm_to_tt fol_tm of Term t => t | _ => error "fol_tm_to_tt: Term expected"  end;
    2.89 +  in
    2.90 +    case tm_to_tt fol_tm of
    2.91 +      Term t => t
    2.92 +    | _ => error "fol_tm_to_tt: Term expected"
    2.93 +  end
    2.94  
    2.95  (*Maps fully-typed metis terms to isabelle terms*)
    2.96 -fun fol_term_to_hol_FT ctxt fol_tm =
    2.97 -  let val _ = trace_msg (fn () => "fol_term_to_hol_FT: " ^ Metis.Term.toString fol_tm)
    2.98 +fun hol_term_from_fol_FT ctxt fol_tm =
    2.99 +  let val _ = trace_msg (fn () => "hol_term_from_fol_FT: " ^
   2.100 +                                  Metis.Term.toString fol_tm)
   2.101        fun cvt (Metis.Term.Fn ("ti", [Metis.Term.Var v, _])) =
   2.102               (case strip_prefix schematic_var_prefix v of
   2.103                    SOME w =>  mk_var(w, dummyT)
   2.104 @@ -302,7 +331,7 @@
   2.105                | NONE => (*Not a constant. Is it a fixed variable??*)
   2.106              case strip_prefix fixed_var_prefix x of
   2.107                  SOME v => Free (v, fol_type_to_isa ctxt ty)
   2.108 -              | NONE => error ("fol_term_to_hol_FT bad constant: " ^ x))
   2.109 +              | NONE => error ("hol_term_from_fol_FT bad constant: " ^ x))
   2.110          | cvt (Metis.Term.Fn ("ti", [Metis.Term.Fn (".",[tm1,tm2]), _])) =
   2.111              cvt tm1 $ cvt tm2
   2.112          | cvt (Metis.Term.Fn (".",[tm1,tm2])) = (*untyped application*)
   2.113 @@ -316,21 +345,22 @@
   2.114                | NONE => (*Not a constant. Is it a fixed variable??*)
   2.115              case strip_prefix fixed_var_prefix x of
   2.116                  SOME v => Free (v, dummyT)
   2.117 -              | NONE => (trace_msg (fn () => "fol_term_to_hol_FT bad const: " ^ x);
   2.118 -                  fol_term_to_hol_RAW ctxt t))
   2.119 -        | cvt t = (trace_msg (fn () => "fol_term_to_hol_FT bad term: " ^ Metis.Term.toString t);
   2.120 -            fol_term_to_hol_RAW ctxt t)
   2.121 -  in  cvt fol_tm   end;
   2.122 +              | NONE => (trace_msg (fn () => "hol_term_from_fol_FT bad const: " ^ x);
   2.123 +                  hol_term_from_fol_PT ctxt t))
   2.124 +        | cvt t = (trace_msg (fn () => "hol_term_from_fol_FT bad term: " ^ Metis.Term.toString t);
   2.125 +            hol_term_from_fol_PT ctxt t)
   2.126 +  in fol_tm |> cvt end
   2.127  
   2.128 -fun fol_term_to_hol ctxt FO = fol_term_to_hol_RAW ctxt
   2.129 -  | fol_term_to_hol ctxt HO = fol_term_to_hol_RAW ctxt
   2.130 -  | fol_term_to_hol ctxt FT = fol_term_to_hol_FT ctxt;
   2.131 +fun hol_term_from_fol FT = hol_term_from_fol_FT
   2.132 +  | hol_term_from_fol _ = hol_term_from_fol_PT
   2.133  
   2.134 -fun fol_terms_to_hol ctxt mode fol_tms =
   2.135 -  let val ts = map (fol_term_to_hol ctxt mode) fol_tms
   2.136 +fun hol_terms_from_fol ctxt mode skolem_somes fol_tms =
   2.137 +  let val thy = ProofContext.theory_of ctxt
   2.138 +      val ts = map (hol_term_from_fol mode ctxt) fol_tms
   2.139        val _ = trace_msg (fn () => "  calling type inference:")
   2.140        val _ = app (fn t => trace_msg (fn () => Syntax.string_of_term ctxt t)) ts
   2.141 -      val ts' = infer_types ctxt ts;
   2.142 +      val ts' =
   2.143 +        ts |> map (reintroduce_skolem_Eps thy skolem_somes) |> infer_types ctxt
   2.144        val _ = app (fn t => trace_msg
   2.145                      (fn () => "  final term: " ^ Syntax.string_of_term ctxt t ^
   2.146                                "  of type  " ^ Syntax.string_of_typ ctxt (type_of t)))
   2.147 @@ -371,22 +401,23 @@
   2.148      (*This causes variables to have an index of 1 by default. SEE ALSO mk_var above.*)
   2.149  
   2.150  (* INFERENCE RULE: ASSUME *)
   2.151 -fun assume_inf ctxt mode atm =
   2.152 +fun assume_inf ctxt mode skolem_somes atm =
   2.153    inst_excluded_middle
   2.154      (ProofContext.theory_of ctxt)
   2.155 -    (singleton (fol_terms_to_hol ctxt mode) (Metis.Term.Fn atm));
   2.156 +    (singleton (hol_terms_from_fol ctxt mode skolem_somes) (Metis.Term.Fn atm))
   2.157  
   2.158  (* INFERENCE RULE: INSTANTIATE (Subst). Type instantiations are ignored. Trying to reconstruct
   2.159     them admits new possibilities of errors, e.g. concerning sorts. Instead we try to arrange
   2.160     that new TVars are distinct and that types can be inferred from terms.*)
   2.161 -fun inst_inf ctxt mode thpairs fsubst th =
   2.162 +fun inst_inf ctxt mode skolem_somes thpairs fsubst th =
   2.163    let val thy = ProofContext.theory_of ctxt
   2.164        val i_th   = lookth thpairs th
   2.165        val i_th_vars = Term.add_vars (prop_of i_th) []
   2.166        fun find_var x = the (List.find (fn ((a,_),_) => a=x) i_th_vars)
   2.167        fun subst_translation (x,y) =
   2.168              let val v = find_var x
   2.169 -                val t = fol_term_to_hol ctxt mode y (*we call infer_types below*)
   2.170 +                (* We call "reintroduce_skolem_Eps" and "infer_types" below. *)
   2.171 +                val t = hol_term_from_fol mode ctxt y
   2.172              in  SOME (cterm_of thy (Var v), t)  end
   2.173              handle Option =>
   2.174                  (trace_msg (fn() => "List.find failed for the variable " ^ x ^
   2.175 @@ -401,7 +432,8 @@
   2.176        val _ = trace_msg (fn () => "  isa th: " ^ Display.string_of_thm ctxt i_th)
   2.177        val substs = map_filter remove_typeinst (Metis.Subst.toList fsubst)
   2.178        val (vars,rawtms) = ListPair.unzip (map_filter subst_translation substs)
   2.179 -      val tms = infer_types ctxt rawtms;
   2.180 +      val tms = rawtms |> map (reintroduce_skolem_Eps thy skolem_somes)
   2.181 +                       |> infer_types ctxt
   2.182        val ctm_of = cterm_incr_types thy (1 + Thm.maxidx_of i_th)
   2.183        val substs' = ListPair.zip (vars, map ctm_of tms)
   2.184        val _ = trace_msg (fn () =>
   2.185 @@ -409,10 +441,11 @@
   2.186            (substs' |> map (fn (x, y) =>
   2.187              Syntax.string_of_term ctxt (term_of x) ^ " |-> " ^
   2.188              Syntax.string_of_term ctxt (term_of y)))));
   2.189 -  in  cterm_instantiate substs' i_th end
   2.190 +  in cterm_instantiate substs' i_th end
   2.191    handle THM (msg, _, _) => error ("metis error (inst_inf):\n" ^ msg)
   2.192         | ERROR msg => error ("metis error (inst_inf):\n" ^ msg ^
   2.193 -                             "\n(Perhaps you want to try \"metisFT\".)")
   2.194 +                             "\n(Perhaps you want to try \"metisFT\" if you \
   2.195 +                             \haven't done so already.)")
   2.196  
   2.197  (* INFERENCE RULE: RESOLVE *)
   2.198  
   2.199 @@ -428,7 +461,7 @@
   2.200        | _ => raise THM ("resolve_inc_tyvars: unique result expected", i, [tha,thb])
   2.201    end;
   2.202  
   2.203 -fun resolve_inf ctxt mode thpairs atm th1 th2 =
   2.204 +fun resolve_inf ctxt mode skolem_somes thpairs atm th1 th2 =
   2.205    let
   2.206      val i_th1 = lookth thpairs th1 and i_th2 = lookth thpairs th2
   2.207      val _ = trace_msg (fn () => "  isa th1 (pos): " ^ Display.string_of_thm ctxt i_th1)
   2.208 @@ -438,7 +471,8 @@
   2.209      else if is_TrueI i_th2 then i_th1
   2.210      else
   2.211        let
   2.212 -        val i_atm = singleton (fol_terms_to_hol ctxt mode) (Metis.Term.Fn atm)
   2.213 +        val i_atm = singleton (hol_terms_from_fol ctxt mode skolem_somes)
   2.214 +                              (Metis.Term.Fn atm)
   2.215          val _ = trace_msg (fn () => "  atom: " ^ Syntax.string_of_term ctxt i_atm)
   2.216          val prems_th1 = prems_of i_th1
   2.217          val prems_th2 = prems_of i_th2
   2.218 @@ -455,9 +489,9 @@
   2.219  val refl_x = cterm_of @{theory} (Var (hd (Term.add_vars (prop_of REFL_THM) [])));
   2.220  val refl_idx = 1 + Thm.maxidx_of REFL_THM;
   2.221  
   2.222 -fun refl_inf ctxt mode t =
   2.223 +fun refl_inf ctxt mode skolem_somes t =
   2.224    let val thy = ProofContext.theory_of ctxt
   2.225 -      val i_t = singleton (fol_terms_to_hol ctxt mode) t
   2.226 +      val i_t = singleton (hol_terms_from_fol ctxt mode skolem_somes) t
   2.227        val _ = trace_msg (fn () => "  term: " ^ Syntax.string_of_term ctxt i_t)
   2.228        val c_t = cterm_incr_types thy refl_idx i_t
   2.229    in  cterm_instantiate [(refl_x, c_t)] REFL_THM  end;
   2.230 @@ -467,10 +501,10 @@
   2.231    | get_ty_arg_size _ _ = 0;
   2.232  
   2.233  (* INFERENCE RULE: EQUALITY *)
   2.234 -fun equality_inf ctxt mode (pos, atm) fp fr =
   2.235 +fun equality_inf ctxt mode skolem_somes (pos, atm) fp fr =
   2.236    let val thy = ProofContext.theory_of ctxt
   2.237        val m_tm = Metis.Term.Fn atm
   2.238 -      val [i_atm,i_tm] = fol_terms_to_hol ctxt mode [m_tm, fr]
   2.239 +      val [i_atm,i_tm] = hol_terms_from_fol ctxt mode skolem_somes [m_tm, fr]
   2.240        val _ = trace_msg (fn () => "sign of the literal: " ^ Bool.toString pos)
   2.241        fun replace_item_list lx 0 (_::ls) = lx::ls
   2.242          | replace_item_list lx i (l::ls) = l :: replace_item_list lx (i-1) ls
   2.243 @@ -539,24 +573,28 @@
   2.244  
   2.245  val factor = Seq.hd o distinct_subgoals_tac;
   2.246  
   2.247 -fun step _ _ thpairs (fol_th, Metis.Proof.Axiom _) = factor (axiom_inf thpairs fol_th)
   2.248 -  | step ctxt mode _ (_, Metis.Proof.Assume f_atm) = assume_inf ctxt mode f_atm
   2.249 -  | step ctxt mode thpairs (_, Metis.Proof.Subst (f_subst, f_th1)) =
   2.250 -      factor (inst_inf ctxt mode thpairs f_subst f_th1)
   2.251 -  | step ctxt mode thpairs (_, Metis.Proof.Resolve(f_atm, f_th1, f_th2)) =
   2.252 -      factor (resolve_inf ctxt mode thpairs f_atm f_th1 f_th2)
   2.253 -  | step ctxt mode _ (_, Metis.Proof.Refl f_tm) = refl_inf ctxt mode f_tm
   2.254 -  | step ctxt mode _ (_, Metis.Proof.Equality (f_lit, f_p, f_r)) =
   2.255 -      equality_inf ctxt mode f_lit f_p f_r;
   2.256 +fun step ctxt mode skolem_somes thpairs p =
   2.257 +  case p of
   2.258 +    (fol_th, Metis.Proof.Axiom _) => factor (axiom_inf thpairs fol_th)
   2.259 +  | (_, Metis.Proof.Assume f_atm) => assume_inf ctxt mode skolem_somes f_atm
   2.260 +  | (_, Metis.Proof.Subst (f_subst, f_th1)) =>
   2.261 +    factor (inst_inf ctxt mode skolem_somes thpairs f_subst f_th1)
   2.262 +  | (_, Metis.Proof.Resolve(f_atm, f_th1, f_th2)) =>
   2.263 +    factor (resolve_inf ctxt mode skolem_somes thpairs f_atm f_th1 f_th2)
   2.264 +  | (_, Metis.Proof.Refl f_tm) => refl_inf ctxt mode skolem_somes f_tm
   2.265 +  | (_, Metis.Proof.Equality (f_lit, f_p, f_r)) =>
   2.266 +    equality_inf ctxt mode skolem_somes f_lit f_p f_r
   2.267  
   2.268  fun real_literal (_, (c, _)) = not (String.isPrefix class_prefix c);
   2.269  
   2.270 -fun translate _ _ thpairs [] = thpairs
   2.271 -  | translate mode ctxt thpairs ((fol_th, inf) :: infpairs) =
   2.272 +(* TODO: use "fold" instead *)
   2.273 +fun translate _ _ _ thpairs [] = thpairs
   2.274 +  | translate ctxt mode skolem_somes thpairs ((fol_th, inf) :: infpairs) =
   2.275        let val _ = trace_msg (fn () => "=============================================")
   2.276            val _ = trace_msg (fn () => "METIS THM: " ^ Metis.Thm.toString fol_th)
   2.277            val _ = trace_msg (fn () => "INFERENCE: " ^ Metis.Proof.inferenceToString inf)
   2.278 -          val th = Meson.flexflex_first_order (step ctxt mode thpairs (fol_th, inf))
   2.279 +          val th = Meson.flexflex_first_order (step ctxt mode skolem_somes
   2.280 +                                                    thpairs (fol_th, inf))
   2.281            val _ = trace_msg (fn () => "ISABELLE THM: " ^ Display.string_of_thm ctxt th)
   2.282            val _ = trace_msg (fn () => "=============================================")
   2.283            val n_metis_lits =
   2.284 @@ -564,7 +602,7 @@
   2.285        in
   2.286            if nprems_of th = n_metis_lits then ()
   2.287            else error "Metis: proof reconstruction has gone wrong";
   2.288 -          translate mode ctxt ((fol_th, th) :: thpairs) infpairs
   2.289 +          translate ctxt mode skolem_somes ((fol_th, th) :: thpairs) infpairs
   2.290        end;
   2.291  
   2.292  (*Determining which axiom clauses are actually used*)
   2.293 @@ -592,7 +630,8 @@
   2.294  
   2.295  type logic_map =
   2.296    {axioms: (Metis.Thm.thm * thm) list,
   2.297 -   tfrees: type_literal list};
   2.298 +   tfrees: type_literal list,
   2.299 +   skolem_somes: (string * (typ * term list * term)) list}
   2.300  
   2.301  fun const_in_metis c (pred, tm_list) =
   2.302    let
   2.303 @@ -610,14 +649,15 @@
   2.304  
   2.305  (*transform isabelle type / arity clause to metis clause *)
   2.306  fun add_type_thm [] lmap = lmap
   2.307 -  | add_type_thm ((ith, mth) :: cls) {axioms, tfrees} =
   2.308 -      add_type_thm cls {axioms = (mth, ith) :: axioms,
   2.309 -                        tfrees = tfrees}
   2.310 +  | add_type_thm ((ith, mth) :: cls) {axioms, tfrees, skolem_somes} =
   2.311 +      add_type_thm cls {axioms = (mth, ith) :: axioms, tfrees = tfrees,
   2.312 +                        skolem_somes = skolem_somes}
   2.313  
   2.314  (*Insert non-logical axioms corresponding to all accumulated TFrees*)
   2.315 -fun add_tfrees {axioms, tfrees} : logic_map =
   2.316 -     {axioms = (map (fn tf => (metis_of_tfree tf, TrueI)) (distinct op= tfrees)) @ axioms,
   2.317 -      tfrees = tfrees};
   2.318 +fun add_tfrees {axioms, tfrees, skolem_somes} : logic_map =
   2.319 +     {axioms = map (rpair TrueI o metis_of_tfree) (distinct (op =) tfrees) @
   2.320 +               axioms,
   2.321 +      tfrees = tfrees, skolem_somes = skolem_somes}
   2.322  
   2.323  fun string_of_mode FO = "FO"
   2.324    | string_of_mode HO = "HO"
   2.325 @@ -628,18 +668,26 @@
   2.326    let val thy = ProofContext.theory_of ctxt
   2.327        (*The modes FO and FT are sticky. HO can be downgraded to FO.*)
   2.328        fun set_mode FO = FO
   2.329 -        | set_mode HO = if forall (Meson.is_fol_term thy o prop_of) (cls@ths) then FO else HO
   2.330 +        | set_mode HO =
   2.331 +          if forall (is_quasi_fol_term thy o prop_of) (cls @ ths) then FO
   2.332 +          else HO
   2.333          | set_mode FT = FT
   2.334        val mode = set_mode mode0
   2.335        (*transform isabelle clause to metis clause *)
   2.336 -      fun add_thm is_conjecture ith {axioms, tfrees} : logic_map =
   2.337 -        let val (mth, tfree_lits) = hol_thm_to_fol is_conjecture ctxt mode ith
   2.338 +      fun add_thm is_conjecture ith {axioms, tfrees, skolem_somes} : logic_map =
   2.339 +        let
   2.340 +          val (mth, tfree_lits, skolem_somes) =
   2.341 +            hol_thm_to_fol is_conjecture ctxt mode (length axioms) skolem_somes
   2.342 +                           ith
   2.343          in
   2.344             {axioms = (mth, Meson.make_meta_clause ith) :: axioms,
   2.345 -            tfrees = union (op =) tfree_lits tfrees}
   2.346 +            tfrees = union (op =) tfree_lits tfrees,
   2.347 +            skolem_somes = skolem_somes}
   2.348          end;
   2.349 -      val lmap0 = fold (add_thm true) cls {axioms = [], tfrees = init_tfrees ctxt}
   2.350 -      val lmap = fold (add_thm false) ths (add_tfrees lmap0)
   2.351 +      val lmap = {axioms = [], tfrees = init_tfrees ctxt, skolem_somes = []}
   2.352 +                 |> fold (add_thm true) cls
   2.353 +                 |> add_tfrees
   2.354 +                 |> fold (add_thm false) ths
   2.355        val clause_lists = map (Metis.Thm.clause o #1) (#axioms lmap)
   2.356        fun used c = exists (Metis.LiteralSet.exists (const_in_metis c o #2)) clause_lists
   2.357        (*Now check for the existence of certain combinators*)
   2.358 @@ -649,10 +697,11 @@
   2.359        val thC   = if used "c_COMBC" then [cnf_th @{theory} @{thm COMBC_def}] else []
   2.360        val thS   = if used "c_COMBS" then [cnf_th @{theory} @{thm COMBS_def}] else []
   2.361        val thEQ  = if used "c_fequal" then [cnf_th @{theory} @{thm fequal_imp_equal}, cnf_th @{theory} @{thm equal_imp_fequal}] else []
   2.362 -      val lmap' = if mode=FO then lmap
   2.363 -                  else fold (add_thm false) (thEQ @ thS @ thC @ thB @ thK @ thI) lmap
   2.364 +      val lmap =
   2.365 +        lmap |> mode <> FO
   2.366 +                ? fold (add_thm false) (thEQ @ thS @ thC @ thB @ thK @ thI)
   2.367    in
   2.368 -      (mode, add_type_thm (type_ext thy (map prop_of (cls @ ths))) lmap')
   2.369 +      (mode, add_type_thm (type_ext thy (map prop_of (cls @ ths))) lmap)
   2.370    end;
   2.371  
   2.372  fun refute cls =
   2.373 @@ -664,7 +713,7 @@
   2.374  
   2.375  exception METIS of string;
   2.376  
   2.377 -(* Main function to start metis prove and reconstruction *)
   2.378 +(* Main function to start metis proof and reconstruction *)
   2.379  fun FOL_SOLVE mode ctxt cls ths0 =
   2.380    let val thy = ProofContext.theory_of ctxt
   2.381        val th_cls_pairs =
   2.382 @@ -674,7 +723,7 @@
   2.383        val _ = app (fn th => trace_msg (fn () => Display.string_of_thm ctxt th)) cls
   2.384        val _ = trace_msg (fn () => "THEOREM CLAUSES")
   2.385        val _ = app (fn th => trace_msg (fn () => Display.string_of_thm ctxt th)) ths
   2.386 -      val (mode, {axioms,tfrees}) = build_map mode ctxt cls ths
   2.387 +      val (mode, {axioms, tfrees, skolem_somes}) = build_map mode ctxt cls ths
   2.388        val _ = if null tfrees then ()
   2.389                else (trace_msg (fn () => "TFREE CLAUSES");
   2.390                      app (fn tf => trace_msg (fn _ => tptp_of_type_literal true tf NONE |> fst)) tfrees)
   2.391 @@ -694,7 +743,7 @@
   2.392                  val ctxt' = fold Variable.declare_constraints (map prop_of cls) ctxt
   2.393                               (*add constraints arising from converting goal to clause form*)
   2.394                  val proof = Metis.Proof.proof mth
   2.395 -                val result = translate mode ctxt' axioms proof
   2.396 +                val result = translate ctxt' mode skolem_somes axioms proof
   2.397                  and used = map_filter (used_axioms axioms) proof
   2.398                  val _ = trace_msg (fn () => "METIS COMPLETED...clauses actually used:")
   2.399                  val _ = app (fn th => trace_msg (fn () => Display.string_of_thm ctxt th)) used
     3.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_fact_filter.ML	Fri Jun 11 17:07:27 2010 +0200
     3.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_fact_filter.ML	Fri Jun 11 17:10:23 2010 +0200
     3.3 @@ -21,6 +21,7 @@
     3.4    val tvar_classes_of_terms : term list -> string list
     3.5    val tfree_classes_of_terms : term list -> string list
     3.6    val type_consts_of_terms : theory -> term list -> string list
     3.7 +  val is_quasi_fol_term : theory -> term -> bool
     3.8    val relevant_facts :
     3.9      bool -> bool -> real -> real -> bool -> int -> bool -> relevance_override
    3.10      -> Proof.context * (thm list * 'a) -> thm list
    3.11 @@ -116,6 +117,8 @@
    3.12        add_const_typ_table (const_with_typ thy (c,typ), tab) 
    3.13    | add_term_consts_typs_rm thy (Free(c, typ), tab) =
    3.14        add_const_typ_table (const_with_typ thy (c,typ), tab) 
    3.15 +  | add_term_consts_typs_rm _ (Const (@{const_name skolem_Eps}, _) $ _, tab) =
    3.16 +      tab
    3.17    | add_term_consts_typs_rm thy (t $ u, tab) =
    3.18        add_term_consts_typs_rm thy (t, add_term_consts_typs_rm thy (u, tab))
    3.19    | add_term_consts_typs_rm thy (Abs(_,_,t), tab) = add_term_consts_typs_rm thy (t, tab)
    3.20 @@ -368,38 +371,35 @@
    3.21  
    3.22      fun valid_facts facts =
    3.23        (facts, []) |-> Facts.fold_static (fn (name, ths0) =>
    3.24 -        let
    3.25 -          fun check_thms a =
    3.26 -            (case try (ProofContext.get_thms ctxt) a of
    3.27 -              NONE => false
    3.28 -            | SOME ths1 => Thm.eq_thms (ths0, ths1));
    3.29 +        if Facts.is_concealed facts name orelse
    3.30 +           (respect_no_atp andalso is_package_def name) orelse
    3.31 +           member (op =) multi_base_blacklist (Long_Name.base_name name) then
    3.32 +          I
    3.33 +        else
    3.34 +          let
    3.35 +            fun check_thms a =
    3.36 +              (case try (ProofContext.get_thms ctxt) a of
    3.37 +                NONE => false
    3.38 +              | SOME ths1 => Thm.eq_thms (ths0, ths1));
    3.39  
    3.40 -          val name1 = Facts.extern facts name;
    3.41 -          val name2 = Name_Space.extern full_space name;
    3.42 -          val ths = filter_out is_theorem_bad_for_atps ths0;
    3.43 -        in
    3.44 -          if Facts.is_concealed facts name orelse
    3.45 -             (respect_no_atp andalso is_package_def name) then
    3.46 -            I
    3.47 -          else case find_first check_thms [name1, name2, name] of
    3.48 -            NONE => I
    3.49 -          | SOME name' =>
    3.50 -            cons (name' |> forall (member Thm.eq_thm chained_ths) ths
    3.51 -                           ? prefix chained_prefix, ths)
    3.52 -        end);
    3.53 +            val name1 = Facts.extern facts name;
    3.54 +            val name2 = Name_Space.extern full_space name;
    3.55 +            val ths = filter_out is_theorem_bad_for_atps ths0;
    3.56 +          in
    3.57 +            case find_first check_thms [name1, name2, name] of
    3.58 +              NONE => I
    3.59 +            | SOME name' =>
    3.60 +              cons (name' |> forall (member Thm.eq_thm chained_ths) ths
    3.61 +                             ? prefix chained_prefix, ths)
    3.62 +          end)
    3.63    in valid_facts global_facts @ valid_facts local_facts end;
    3.64  
    3.65  fun multi_name a th (n, pairs) =
    3.66    (n + 1, (a ^ "(" ^ Int.toString n ^ ")", th) :: pairs);
    3.67  
    3.68 -fun add_single_names (a, []) pairs = pairs
    3.69 -  | add_single_names (a, [th]) pairs = (a, th) :: pairs
    3.70 -  | add_single_names (a, ths) pairs = #2 (fold (multi_name a) ths (1, pairs));
    3.71 -
    3.72 -(*Ignore blacklisted basenames*)
    3.73 -fun add_multi_names (a, ths) pairs =
    3.74 -  if member (op =) multi_base_blacklist (Long_Name.base_name a) then pairs
    3.75 -  else add_single_names (a, ths) pairs;
    3.76 +fun add_names (a, []) pairs = pairs
    3.77 +  | add_names (a, [th]) pairs = (a, th) :: pairs
    3.78 +  | add_names (a, ths) pairs = #2 (fold (multi_name a) ths (1, pairs))
    3.79  
    3.80  fun is_multi (a, ths) = length ths > 1 orelse String.isSuffix ".axioms" a;
    3.81  
    3.82 @@ -408,8 +408,7 @@
    3.83  fun name_thm_pairs respect_no_atp ctxt name_thms_pairs =
    3.84    let
    3.85      val (mults, singles) = List.partition is_multi name_thms_pairs
    3.86 -    val ps = [] |> fold add_single_names singles
    3.87 -                |> fold add_multi_names mults
    3.88 +    val ps = [] |> fold add_names singles |> fold add_names mults
    3.89    in ps |> respect_no_atp ? filter_out (No_ATPs.member ctxt o snd) end;
    3.90  
    3.91  fun is_named ("", th) =
    3.92 @@ -472,8 +471,11 @@
    3.93  (* ATP invocation methods setup                                *)
    3.94  (***************************************************************)
    3.95  
    3.96 +fun is_quasi_fol_term thy = Meson.is_fol_term thy o snd o kill_skolem_Eps ~1 []
    3.97 +
    3.98  (*Ensures that no higher-order theorems "leak out"*)
    3.99 -fun restrict_to_logic thy true cls = filter (Meson.is_fol_term thy o prop_of o fst) cls
   3.100 +fun restrict_to_logic thy true cls =
   3.101 +    filter (is_quasi_fol_term thy o prop_of o fst) cls
   3.102    | restrict_to_logic thy false cls = cls;
   3.103  
   3.104  (**** Predicates to detect unwanted clauses (prolific or likely to cause
   3.105 @@ -531,7 +533,7 @@
   3.106  fun remove_dangerous_clauses full_types add_thms =
   3.107    filter_out (is_dangerous_theorem full_types add_thms o fst)
   3.108  
   3.109 -fun is_first_order thy = forall (Meson.is_fol_term thy) o map prop_of
   3.110 +fun is_fol_goal thy = forall (Meson.is_fol_term thy) o map prop_of
   3.111  
   3.112  fun relevant_facts full_types respect_no_atp relevance_threshold
   3.113                     relevance_convergence defs_relevant max_new theory_relevant
   3.114 @@ -542,17 +544,17 @@
   3.115    else
   3.116      let
   3.117        val thy = ProofContext.theory_of ctxt
   3.118 -      val add_thms = cnf_for_facts ctxt add
   3.119        val has_override = not (null add) orelse not (null del)
   3.120 -      val is_FO = is_first_order thy goal_cls
   3.121 +      val is_FO = is_fol_goal thy goal_cls
   3.122        val axioms =
   3.123 -        checked_name_thm_pairs respect_no_atp ctxt
   3.124 +        checked_name_thm_pairs (respect_no_atp andalso not only) ctxt
   3.125              (if only then map (name_thms_pair_from_ref ctxt chained_ths) add
   3.126               else all_name_thms_pairs respect_no_atp ctxt chained_ths)
   3.127          |> cnf_rules_pairs thy
   3.128          |> not has_override ? make_unique
   3.129 -        |> restrict_to_logic thy is_FO
   3.130 -        |> not only ? remove_dangerous_clauses full_types add_thms
   3.131 +        |> not only ? restrict_to_logic thy is_FO
   3.132 +        |> (if only then I
   3.133 +            else remove_dangerous_clauses full_types (cnf_for_facts ctxt add))
   3.134      in
   3.135        relevance_filter ctxt relevance_threshold relevance_convergence
   3.136                         defs_relevant max_new theory_relevant relevance_override
   3.137 @@ -564,7 +566,7 @@
   3.138     create additional clauses based on the information from extra_cls *)
   3.139  fun prepare_clauses dfg goal_cls chained_ths axcls extra_cls thy =
   3.140    let
   3.141 -    val is_FO = is_first_order thy goal_cls
   3.142 +    val is_FO = is_fol_goal thy goal_cls
   3.143      val ccls = subtract_cls extra_cls goal_cls
   3.144      val _ = app (fn th => trace_msg (fn _ => Display.string_of_thm_global thy th)) ccls
   3.145      val ccltms = map prop_of ccls
   3.146 @@ -576,7 +578,7 @@
   3.147      val conjectures = make_conjecture_clauses dfg thy ccls
   3.148      val (_, extra_clauses) = ListPair.unzip (make_axiom_clauses dfg thy extra_cls)
   3.149      val (clnames, axiom_clauses) = ListPair.unzip (make_axiom_clauses dfg thy axcls)
   3.150 -    val helper_clauses = get_helper_clauses dfg thy is_FO (conjectures, extra_cls, [])
   3.151 +    val helper_clauses = get_helper_clauses dfg thy is_FO conjectures extra_cls
   3.152      val (supers', arity_clauses) = make_arity_clauses_dfg dfg thy tycons supers
   3.153      val classrel_clauses = make_classrel_clauses thy subs supers'
   3.154    in
     4.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_fact_preprocessor.ML	Fri Jun 11 17:07:27 2010 +0200
     4.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_fact_preprocessor.ML	Fri Jun 11 17:10:23 2010 +0200
     4.3 @@ -10,8 +10,11 @@
     4.4    val chained_prefix: string
     4.5    val trace: bool Unsynchronized.ref
     4.6    val trace_msg: (unit -> string) -> unit
     4.7 +  val skolem_Eps_pseudo_theory: string
     4.8    val skolem_prefix: string
     4.9    val skolem_infix: string
    4.10 +  val is_skolem_const_name: string -> bool
    4.11 +  val skolem_type_and_args: typ -> term -> typ * term list
    4.12    val cnf_axiom: theory -> thm -> thm list
    4.13    val multi_base_blacklist: string list
    4.14    val is_theorem_bad_for_atps: thm -> bool
    4.15 @@ -39,6 +42,7 @@
    4.16  val trace = Unsynchronized.ref false;
    4.17  fun trace_msg msg = if !trace then tracing (msg ()) else ();
    4.18  
    4.19 +val skolem_Eps_pseudo_theory = "Sledgehammer.Eps"
    4.20  val skolem_prefix = "sko_"
    4.21  val skolem_infix = "$"
    4.22  
    4.23 @@ -72,13 +76,22 @@
    4.24  
    4.25  (**** SKOLEMIZATION BY INFERENCE (lcp) ****)
    4.26  
    4.27 +fun skolem_Eps_const T =
    4.28 +  Const (@{const_name skolem_Eps}, (T --> HOLogic.boolT) --> T)
    4.29 +
    4.30  (*Keep the full complexity of the original name*)
    4.31  fun flatten_name s = space_implode "_X" (Long_Name.explode s);
    4.32  
    4.33 -fun skolem_name thm_name nref var_name =
    4.34 -  skolem_prefix ^ thm_name ^ "_" ^ Int.toString (Unsynchronized.inc nref) ^
    4.35 +fun skolem_name thm_name j var_name =
    4.36 +  skolem_prefix ^ thm_name ^ "_" ^ Int.toString j ^
    4.37    skolem_infix ^ (if var_name = "" then "g" else flatten_name var_name)
    4.38  
    4.39 +(* Hack: Could return false positives (e.g., a user happens to declare a
    4.40 +   constant called "SomeTheory.sko_means_shoe_in_$wedish". *)
    4.41 +val is_skolem_const_name =
    4.42 +  Long_Name.base_name
    4.43 +  #> String.isPrefix skolem_prefix andf String.isSubstring skolem_infix
    4.44 +
    4.45  fun rhs_extra_types lhsT rhs =
    4.46    let val lhs_vars = Term.add_tfreesT lhsT []
    4.47        fun add_new_TFrees (TFree v) =
    4.48 @@ -87,34 +100,39 @@
    4.49        val rhs_consts = fold_aterms (fn Const c => insert (op =) c | _ => I) rhs []
    4.50    in fold (#2 #> Term.fold_atyps add_new_TFrees) rhs_consts [] end;
    4.51  
    4.52 +fun skolem_type_and_args bound_T body =
    4.53 +  let
    4.54 +    val args1 = OldTerm.term_frees body
    4.55 +    val Ts1 = map type_of args1
    4.56 +    val Ts2 = rhs_extra_types (Ts1 ---> bound_T) body
    4.57 +    val args2 = map (fn T => Free (gensym "vsk", T)) Ts2
    4.58 +  in (Ts2 ---> Ts1 ---> bound_T, args2 @ args1) end
    4.59 +
    4.60  (* Traverse a theorem, declaring Skolem function definitions. String "s" is the
    4.61     suggested prefix for the Skolem constants. *)
    4.62  fun declare_skolem_funs s th thy =
    4.63    let
    4.64 -    val nref = Unsynchronized.ref 0    (* FIXME ??? *)
    4.65 -    fun dec_sko (Const (@{const_name Ex}, _) $ (xtp as Abs (s', T, p))) (axs, thy) =
    4.66 -          (*Existential: declare a Skolem function, then insert into body and continue*)
    4.67 -          let
    4.68 -            val cname = skolem_name s nref s'
    4.69 -            val args0 = OldTerm.term_frees xtp  (*get the formal parameter list*)
    4.70 -            val Ts = map type_of args0
    4.71 -            val extraTs = rhs_extra_types (Ts ---> T) xtp
    4.72 -            val argsx = map (fn T => Free (gensym "vsk", T)) extraTs
    4.73 -            val args = argsx @ args0
    4.74 -            val cT = extraTs ---> Ts ---> T
    4.75 -            val rhs = list_abs_free (map dest_Free args, HOLogic.choice_const T $ xtp)
    4.76 -                    (*Forms a lambda-abstraction over the formal parameters*)
    4.77 -            val (c, thy) =
    4.78 -              Sign.declare_const ((Binding.conceal (Binding.name cname), cT), NoSyn) thy
    4.79 -            val cdef = cname ^ "_def"
    4.80 -            val ((_, ax), thy) =
    4.81 -              Thm.add_def true false (Binding.name cdef, Logic.mk_equals (c, rhs)) thy
    4.82 -            val ax' = Drule.export_without_context ax
    4.83 -          in dec_sko (subst_bound (list_comb (c, args), p)) (ax' :: axs, thy) end
    4.84 +    val skolem_count = Unsynchronized.ref 0    (* FIXME ??? *)
    4.85 +    fun dec_sko (Const (@{const_name Ex}, _) $ (body as Abs (s', T, p)))
    4.86 +                (axs, thy) =
    4.87 +        (*Existential: declare a Skolem function, then insert into body and continue*)
    4.88 +        let
    4.89 +          val id = skolem_name s (Unsynchronized.inc skolem_count) s'
    4.90 +          val (cT, args) = skolem_type_and_args T body
    4.91 +          val rhs = list_abs_free (map dest_Free args,
    4.92 +                                   skolem_Eps_const T $ body)
    4.93 +                  (*Forms a lambda-abstraction over the formal parameters*)
    4.94 +          val (c, thy) =
    4.95 +            Sign.declare_const ((Binding.conceal (Binding.name id), cT), NoSyn) thy
    4.96 +          val cdef = id ^ "_def"
    4.97 +          val ((_, ax), thy) =
    4.98 +            Thm.add_def true false (Binding.name cdef, Logic.mk_equals (c, rhs)) thy
    4.99 +          val ax' = Drule.export_without_context ax
   4.100 +        in dec_sko (subst_bound (list_comb (c, args), p)) (ax' :: axs, thy) end
   4.101        | dec_sko (Const (@{const_name All}, _) $ (Abs (a, T, p))) thx =
   4.102 -          (*Universal quant: insert a free variable into body and continue*)
   4.103 -          let val fname = Name.variant (OldTerm.add_term_names (p, [])) a
   4.104 -          in dec_sko (subst_bound (Free (fname, T), p)) thx end
   4.105 +        (*Universal quant: insert a free variable into body and continue*)
   4.106 +        let val fname = Name.variant (OldTerm.add_term_names (p, [])) a
   4.107 +        in dec_sko (subst_bound (Free (fname, T), p)) thx end
   4.108        | dec_sko (@{const "op &"} $ p $ q) thx = dec_sko q (dec_sko p thx)
   4.109        | dec_sko (@{const "op |"} $ p $ q) thx = dec_sko q (dec_sko p thx)
   4.110        | dec_sko (@{const Trueprop} $ p) thx = dec_sko p thx
   4.111 @@ -122,29 +140,31 @@
   4.112    in dec_sko (prop_of th) ([], thy) end
   4.113  
   4.114  (*Traverse a theorem, accumulating Skolem function definitions.*)
   4.115 -fun assume_skolem_funs s th =
   4.116 -  let val sko_count = Unsynchronized.ref 0   (* FIXME ??? *)
   4.117 -      fun dec_sko (Const (@{const_name Ex}, _) $ (xtp as Abs (s', T, p))) defs =
   4.118 -            (*Existential: declare a Skolem function, then insert into body and continue*)
   4.119 -            let val skos = map (#1 o Logic.dest_equals) defs  (*existing sko fns*)
   4.120 -                val args = subtract (op =) skos (OldTerm.term_frees xtp) (*the formal parameters*)
   4.121 -                val Ts = map type_of args
   4.122 -                val cT = Ts ---> T
   4.123 -                val id = skolem_name s sko_count s'
   4.124 -                val c = Free (id, cT)
   4.125 -                val rhs = list_abs_free (map dest_Free args,
   4.126 -                                         HOLogic.choice_const T $ xtp)
   4.127 -                      (*Forms a lambda-abstraction over the formal parameters*)
   4.128 -                val def = Logic.mk_equals (c, rhs)
   4.129 -            in dec_sko (subst_bound (list_comb(c,args), p)) (def :: defs) end
   4.130 -        | dec_sko (Const (@{const_name All},_) $ Abs (a, T, p)) defs =
   4.131 -            (*Universal quant: insert a free variable into body and continue*)
   4.132 -            let val fname = Name.variant (OldTerm.add_term_names (p,[])) a
   4.133 -            in dec_sko (subst_bound (Free(fname,T), p)) defs end
   4.134 -        | dec_sko (@{const "op &"} $ p $ q) defs = dec_sko q (dec_sko p defs)
   4.135 -        | dec_sko (@{const "op |"} $ p $ q) defs = dec_sko q (dec_sko p defs)
   4.136 -        | dec_sko (@{const Trueprop} $ p) defs = dec_sko p defs
   4.137 -        | dec_sko t defs = defs (*Do nothing otherwise*)
   4.138 +fun assume_skolem_funs inline s th =
   4.139 +  let
   4.140 +    val skolem_count = Unsynchronized.ref 0   (* FIXME ??? *)
   4.141 +    fun dec_sko (Const (@{const_name Ex}, _) $ (body as Abs (s', T, p))) defs =
   4.142 +        (*Existential: declare a Skolem function, then insert into body and continue*)
   4.143 +        let
   4.144 +          val skos = map (#1 o Logic.dest_equals) defs  (*existing sko fns*)
   4.145 +          val args = subtract (op =) skos (OldTerm.term_frees body) (*the formal parameters*)
   4.146 +          val Ts = map type_of args
   4.147 +          val cT = Ts ---> T (* FIXME: use "skolem_type_and_args" *)
   4.148 +          val id = skolem_name s (Unsynchronized.inc skolem_count) s'
   4.149 +          val c = Free (id, cT)
   4.150 +          val rhs = list_abs_free (map dest_Free args, skolem_Eps_const T $ body)
   4.151 +                (*Forms a lambda-abstraction over the formal parameters*)
   4.152 +          val def = Logic.mk_equals (c, rhs)
   4.153 +          val comb = list_comb (if inline then rhs else c, args)
   4.154 +        in dec_sko (subst_bound (comb, p)) (def :: defs) end
   4.155 +      | dec_sko (Const (@{const_name All},_) $ Abs (a, T, p)) defs =
   4.156 +        (*Universal quant: insert a free variable into body and continue*)
   4.157 +        let val fname = Name.variant (OldTerm.add_term_names (p,[])) a
   4.158 +        in dec_sko (subst_bound (Free(fname,T), p)) defs end
   4.159 +      | dec_sko (@{const "op &"} $ p $ q) defs = dec_sko q (dec_sko p defs)
   4.160 +      | dec_sko (@{const "op |"} $ p $ q) defs = dec_sko q (dec_sko p defs)
   4.161 +      | dec_sko (@{const Trueprop} $ p) defs = dec_sko p defs
   4.162 +      | dec_sko t defs = defs (*Do nothing otherwise*)
   4.163    in  dec_sko (prop_of th) []  end;
   4.164  
   4.165  
   4.166 @@ -273,19 +293,25 @@
   4.167  (*Given the definition of a Skolem function, return a theorem to replace
   4.168    an existential formula by a use of that function.
   4.169     Example: "EX x. x : A & x ~: B ==> sko A B : A & sko A B ~: B"  [.] *)
   4.170 -fun skolem_of_def def =
   4.171 -  let val (c,rhs) = Thm.dest_equals (cprop_of (freeze_thm def))
   4.172 +fun skolem_theorem_of_def inline def =
   4.173 +  let
   4.174 +      val (c,rhs) = Thm.dest_equals (cprop_of (freeze_thm def))
   4.175        val (ch, frees) = c_variant_abs_multi (rhs, [])
   4.176        val (chilbert,cabs) = Thm.dest_comb ch
   4.177        val thy = Thm.theory_of_cterm chilbert
   4.178        val t = Thm.term_of chilbert
   4.179 -      val T = case t of
   4.180 -                Const (@{const_name Eps}, Type (@{type_name fun},[_,T])) => T
   4.181 -              | _ => raise THM ("skolem_of_def: expected Eps", 0, [def])
   4.182 +      val T =
   4.183 +        case t of
   4.184 +          Const (@{const_name skolem_Eps}, Type (@{type_name fun}, [_, T])) => T
   4.185 +        | _ => raise THM ("skolem_theorem_of_def: expected \"Eps\"", 0, [def])
   4.186        val cex = Thm.cterm_of thy (HOLogic.exists_const T)
   4.187        val ex_tm = c_mkTrueprop (Thm.capply cex cabs)
   4.188 -      and conc =  c_mkTrueprop (Drule.beta_conv cabs (Drule.list_comb(c,frees)));
   4.189 -      fun tacf [prem] = rewrite_goals_tac [def] THEN rtac (prem RS @{thm someI_ex}) 1
   4.190 +      and conc =
   4.191 +        Drule.list_comb (if inline then rhs else c, frees)
   4.192 +        |> Drule.beta_conv cabs |> c_mkTrueprop
   4.193 +      fun tacf [prem] =
   4.194 +        (if inline then all_tac else rewrite_goals_tac [def])
   4.195 +        THEN rtac (prem RS @{thm skolem_someI_ex}) 1
   4.196    in  Goal.prove_internal [ex_tm] conc tacf
   4.197         |> forall_intr_list frees
   4.198         |> Thm.forall_elim_vars 0  (*Introduce Vars, but don't discharge defs.*)
   4.199 @@ -303,9 +329,9 @@
   4.200    in  (th3, ctxt)  end;
   4.201  
   4.202  (*Generate Skolem functions for a theorem supplied in nnf*)
   4.203 -fun assume_skolem_of_def s th =
   4.204 -  map (skolem_of_def o Thm.assume o cterm_of (theory_of_thm th))
   4.205 -      (assume_skolem_funs s th)
   4.206 +fun skolem_theorems_of_assume inline s th =
   4.207 +  map (skolem_theorem_of_def inline o Thm.assume o cterm_of (theory_of_thm th))
   4.208 +      (assume_skolem_funs inline s th)
   4.209  
   4.210  
   4.211  (*** Blacklisting (more in "Sledgehammer_Fact_Filter") ***)
   4.212 @@ -364,7 +390,7 @@
   4.213    else gensym "unknown_thm_";
   4.214  
   4.215  (*Skolemize a named theorem, with Skolem functions as additional premises.*)
   4.216 -fun skolem_thm (s, th) =
   4.217 +fun skolemize_theorem s th =
   4.218    if member (op =) multi_base_blacklist (Long_Name.base_name s) orelse
   4.219       is_theorem_bad_for_atps th then
   4.220      []
   4.221 @@ -372,7 +398,8 @@
   4.222      let
   4.223        val ctxt0 = Variable.global_thm_context th
   4.224        val (nnfth, ctxt) = to_nnf th ctxt0
   4.225 -      val defs = assume_skolem_of_def s nnfth
   4.226 +      val inline = exists_type (exists_subtype (can dest_TFree)) (prop_of nnfth)
   4.227 +      val defs = skolem_theorems_of_assume inline s nnfth
   4.228        val (cnfs, ctxt) = Meson.make_cnf defs nnfth ctxt
   4.229      in
   4.230        cnfs |> map introduce_combinators
   4.231 @@ -402,7 +429,7 @@
   4.232  fun cnf_axiom thy th0 =
   4.233    let val th = Thm.transfer thy th0 in
   4.234      case lookup_cache thy th of
   4.235 -      NONE => map Thm.close_derivation (skolem_thm (fake_name th, th))
   4.236 +      NONE => map Thm.close_derivation (skolemize_theorem (fake_name th) th)
   4.237      | SOME cls => cls
   4.238    end;
   4.239  
   4.240 @@ -438,7 +465,8 @@
   4.241  
   4.242  fun skolem_cnfs (th, ctxt0, ctxt, nnfth, defs) =
   4.243    let
   4.244 -    val (cnfs, ctxt) = Meson.make_cnf (map skolem_of_def defs) nnfth ctxt;
   4.245 +    val (cnfs, ctxt) =
   4.246 +      Meson.make_cnf (map (skolem_theorem_of_def false) defs) nnfth ctxt
   4.247      val cnfs' = cnfs
   4.248        |> map introduce_combinators
   4.249        |> Variable.export ctxt ctxt0
   4.250 @@ -455,14 +483,17 @@
   4.251        if Facts.is_concealed facts name orelse already_seen thy name then I
   4.252        else cons (name, ths));
   4.253      val new_thms = (new_facts, []) |-> fold (fn (name, ths) =>
   4.254 -      if member (op =) multi_base_blacklist (Long_Name.base_name name) then I
   4.255 -      else fold_index (fn (i, th) =>
   4.256 -        if is_theorem_bad_for_atps th orelse is_some (lookup_cache thy th) then
   4.257 -          I
   4.258 -        else
   4.259 -          cons (name ^ "_" ^ string_of_int (i + 1), Thm.transfer thy th)) ths)
   4.260 +      if member (op =) multi_base_blacklist (Long_Name.base_name name) then
   4.261 +        I
   4.262 +      else
   4.263 +        fold_index (fn (i, th) =>
   4.264 +          if is_theorem_bad_for_atps th orelse is_some (lookup_cache thy th) then
   4.265 +            I
   4.266 +          else
   4.267 +            cons (name ^ "_" ^ string_of_int (i + 1), Thm.transfer thy th)) ths)
   4.268    in
   4.269 -    if null new_facts then NONE
   4.270 +    if null new_facts then
   4.271 +      NONE
   4.272      else
   4.273        let
   4.274          val (defs, thy') = thy
     5.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_hol_clause.ML	Fri Jun 11 17:07:27 2010 +0200
     5.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_hol_clause.ML	Fri Jun 11 17:10:23 2010 +0200
     5.3 @@ -29,14 +29,17 @@
     5.4    val type_of_combterm : combterm -> fol_type
     5.5    val strip_combterm_comb : combterm -> combterm * combterm list
     5.6    val literals_of_term : theory -> term -> literal list * typ list
     5.7 +  val kill_skolem_Eps :
     5.8 +    int -> (string * (typ * term list * term)) list -> term
     5.9 +    -> (string * (typ * term list * term)) list * term
    5.10    exception TRIVIAL
    5.11    val make_conjecture_clauses : bool -> theory -> thm list -> hol_clause list
    5.12    val make_axiom_clauses : bool -> theory ->
    5.13         (thm * (axiom_name * hol_clause_id)) list -> (axiom_name * hol_clause) list
    5.14    val type_wrapper_name : string
    5.15 -  val get_helper_clauses : bool -> theory -> bool ->
    5.16 -       hol_clause list * (thm * (axiom_name * hol_clause_id)) list * string list ->
    5.17 -       hol_clause list
    5.18 +  val get_helper_clauses :
    5.19 +    bool -> theory -> bool -> hol_clause list
    5.20 +      -> (thm * (axiom_name * hol_clause_id)) list -> hol_clause list
    5.21    val write_tptp_file : bool -> bool -> bool -> Path.T ->
    5.22      hol_clause list * hol_clause list * hol_clause list * hol_clause list *
    5.23      classrel_clause list * arity_clause list -> name_pool option * int
    5.24 @@ -115,28 +118,31 @@
    5.25      TyVar (make_schematic_type_var x, string_of_indexname x);
    5.26  
    5.27  
    5.28 -fun const_type_of dfg thy (c,t) =
    5.29 -      let val (tp,ts) = type_of dfg t
    5.30 -      in  (tp, ts, map (simp_type_of dfg) (Sign.const_typargs thy (c,t))) end;
    5.31 -
    5.32  (* convert a Term.term (with combinators) into a combterm, also accummulate sort info *)
    5.33 -fun combterm_of dfg thy (Const(c,t)) =
    5.34 -      let val (tp,ts,tvar_list) = const_type_of dfg thy (c,t)
    5.35 -          val c' = CombConst (`(make_fixed_const dfg) c, tp, tvar_list)
    5.36 +fun combterm_of dfg thy (Const (c, T)) =
    5.37 +      let
    5.38 +        val (tp, ts) = type_of dfg T
    5.39 +        val tvar_list =
    5.40 +          (if String.isPrefix skolem_Eps_pseudo_theory c then
    5.41 +             [] |> Term.add_tvarsT T |> map TVar
    5.42 +           else
    5.43 +             (c, T) |> Sign.const_typargs thy)
    5.44 +          |> map (simp_type_of dfg)
    5.45 +        val c' = CombConst (`(make_fixed_const dfg) c, tp, tvar_list)
    5.46        in  (c',ts)  end
    5.47 -  | combterm_of dfg _ (Free(v,t)) =
    5.48 -      let val (tp,ts) = type_of dfg t
    5.49 +  | combterm_of dfg _ (Free(v, T)) =
    5.50 +      let val (tp,ts) = type_of dfg T
    5.51            val v' = CombConst (`make_fixed_var v, tp, [])
    5.52        in  (v',ts)  end
    5.53 -  | combterm_of dfg _ (Var(v,t)) =
    5.54 -      let val (tp,ts) = type_of dfg t
    5.55 +  | combterm_of dfg _ (Var(v, T)) =
    5.56 +      let val (tp,ts) = type_of dfg T
    5.57            val v' = CombVar ((make_schematic_var v, string_of_indexname v), tp)
    5.58        in  (v',ts)  end
    5.59    | combterm_of dfg thy (P $ Q) =
    5.60        let val (P',tsP) = combterm_of dfg thy P
    5.61            val (Q',tsQ) = combterm_of dfg thy Q
    5.62        in  (CombApp(P',Q'), union (op =) tsP tsQ)  end
    5.63 -  | combterm_of _ _ (t as Abs _) = raise CLAUSE ("HOL CLAUSE", t);
    5.64 +  | combterm_of _ _ (t as Abs _) = raise CLAUSE ("HOL clause", t);
    5.65  
    5.66  fun predicate_of dfg thy ((@{const Not} $ P), polarity) = predicate_of dfg thy (P, not polarity)
    5.67    | predicate_of dfg thy (t,polarity) = (combterm_of dfg thy (Envir.eta_contract t), polarity);
    5.68 @@ -153,36 +159,100 @@
    5.69  fun literals_of_term_dfg dfg thy P = literals_of_term1 dfg thy ([],[]) P;
    5.70  val literals_of_term = literals_of_term_dfg false;
    5.71  
    5.72 +fun skolem_name i j num_T_args =
    5.73 +  skolem_prefix ^ (space_implode "_" (map Int.toString [i, j, num_T_args])) ^
    5.74 +  skolem_infix ^ "g"
    5.75 +
    5.76 +val flip_type =
    5.77 +  map_atyps (fn TFree (s, S) => TVar ((s, 0), S)
    5.78 +              | TVar ((s, 0), S) => TFree (s, S)
    5.79 +              | T as TVar (_, S) => raise TYPE ("nonzero TVar", [T], [])
    5.80 +              | T => T)
    5.81 +val flip_term =
    5.82 +  map_aterms (fn Free (s, T) => Var ((s, 0), T)
    5.83 +               | Var ((s, 0), T) => Free (s, T)
    5.84 +               | t as Var (_, S) => raise TERM ("nonzero Var", [t])
    5.85 +               | t => t)
    5.86 +  #> map_types flip_type
    5.87 +
    5.88 +fun flipped_skolem_type_and_args bound_T body =
    5.89 +  skolem_type_and_args (flip_type bound_T) (flip_term body)
    5.90 +  |>> flip_type ||> map flip_term
    5.91 +
    5.92 +fun triple_aconv ((T1, ts1, t1), (T2, ts2, t2)) =
    5.93 +  T1 = T2 andalso length ts1 = length ts2 andalso
    5.94 +  forall (op aconv) (ts1 ~~ ts2) andalso t1 aconv t2
    5.95 +
    5.96 +fun kill_skolem_Eps i skolem_somes t =
    5.97 +  if exists_Const (curry (op =) @{const_name skolem_Eps} o fst) t then
    5.98 +    let
    5.99 +      fun aux skolem_somes
   5.100 +              (t as (Const (@{const_name skolem_Eps}, eps_T) $ t2)) =
   5.101 +          let
   5.102 +            val bound_T = range_type eps_T
   5.103 +            val (T, args) = flipped_skolem_type_and_args bound_T t2
   5.104 +            val (skolem_somes, s) =
   5.105 +              if i = ~1 then
   5.106 +                (skolem_somes, @{const_name undefined})
   5.107 +              else case AList.find triple_aconv skolem_somes (T, args, t) of
   5.108 +                s :: _ => (skolem_somes, s)
   5.109 +              | _ =>
   5.110 +                let
   5.111 +                  val s = skolem_Eps_pseudo_theory ^ "." ^
   5.112 +                          skolem_name i (length skolem_somes)
   5.113 +                                        (length (Term.add_tvarsT T []))
   5.114 +                in ((s, (T, args, t)) :: skolem_somes, s) end
   5.115 +          in (skolem_somes, list_comb (Const (s, T), args)) end
   5.116 +        | aux skolem_somes (t1 $ t2) =
   5.117 +          let
   5.118 +            val (skolem_somes, t1) = aux skolem_somes t1
   5.119 +            val (skolem_somes, t2) = aux skolem_somes t2
   5.120 +          in (skolem_somes, t1 $ t2) end
   5.121 +        | aux skolem_somes (Abs (s, T, t')) =
   5.122 +          let val (skolem_somes, t') = aux skolem_somes t' in
   5.123 +            (skolem_somes, Abs (s, T, t'))
   5.124 +          end
   5.125 +        | aux skolem_somes t = (skolem_somes, t)
   5.126 +    in aux skolem_somes t end
   5.127 +  else
   5.128 +    (skolem_somes, t)
   5.129 +
   5.130  (* Trivial problem, which resolution cannot handle (empty clause) *)
   5.131  exception TRIVIAL;
   5.132  
   5.133  (* making axiom and conjecture clauses *)
   5.134 -fun make_clause dfg thy (clause_id, axiom_name, kind, th) =
   5.135 -    let val (lits,ctypes_sorts) = literals_of_term_dfg dfg thy (prop_of th)
   5.136 -    in
   5.137 -        if forall isFalse lits then
   5.138 -            raise TRIVIAL
   5.139 -        else
   5.140 -            HOLClause {clause_id = clause_id, axiom_name = axiom_name, th = th,
   5.141 -                       kind = kind, literals = lits, ctypes_sorts = ctypes_sorts}
   5.142 -    end;
   5.143 -
   5.144 -
   5.145 -fun add_axiom_clause dfg thy (th, (name, id)) =
   5.146 -  let val cls = make_clause dfg thy (id, name, Axiom, th) in
   5.147 -    not (isTaut cls) ? cons (name, cls)
   5.148 +fun make_clause dfg thy (clause_id, axiom_name, kind, th) skolem_somes =
   5.149 +  let
   5.150 +    val (skolem_somes, t) =
   5.151 +      th |> prop_of |> kill_skolem_Eps clause_id skolem_somes
   5.152 +    val (lits, ctypes_sorts) = literals_of_term_dfg dfg thy t
   5.153 +  in
   5.154 +    if forall isFalse lits then
   5.155 +      raise TRIVIAL
   5.156 +    else
   5.157 +      (skolem_somes,
   5.158 +       HOLClause {clause_id = clause_id, axiom_name = axiom_name, th = th,
   5.159 +                  kind = kind, literals = lits, ctypes_sorts = ctypes_sorts})
   5.160    end
   5.161  
   5.162 +fun add_axiom_clause dfg thy (th, (name, id)) (skolem_somes, clss) =
   5.163 +  let
   5.164 +    val (skolem_somes, cls) =
   5.165 +      make_clause dfg thy (id, name, Axiom, th) skolem_somes
   5.166 +  in (skolem_somes, clss |> not (isTaut cls) ? cons (name, cls)) end
   5.167 +
   5.168  fun make_axiom_clauses dfg thy clauses =
   5.169 -  fold (add_axiom_clause dfg thy) clauses []
   5.170 +  ([], []) |> fold (add_axiom_clause dfg thy) clauses |> snd
   5.171  
   5.172 -fun make_conjecture_clauses_aux _ _ _ [] = []
   5.173 -  | make_conjecture_clauses_aux dfg thy n (th::ths) =
   5.174 -      make_clause dfg thy (n,"conjecture", Conjecture, th) ::
   5.175 -      make_conjecture_clauses_aux dfg thy (n+1) ths;
   5.176 -
   5.177 -fun make_conjecture_clauses dfg thy = make_conjecture_clauses_aux dfg thy 0;
   5.178 -
   5.179 +fun make_conjecture_clauses dfg thy =
   5.180 +  let
   5.181 +    fun aux _ _ [] = []
   5.182 +      | aux n skolem_somes (th :: ths) =
   5.183 +        let
   5.184 +          val (skolem_somes, cls) =
   5.185 +            make_clause dfg thy (n, "conjecture", Conjecture, th) skolem_somes
   5.186 +        in cls :: aux (n + 1) skolem_somes ths end
   5.187 +  in aux 0 [] end
   5.188  
   5.189  (**********************************************************************)
   5.190  (* convert clause into ATP specific formats:                          *)
   5.191 @@ -415,19 +485,16 @@
   5.192  
   5.193  fun count_clause (HOLClause {literals, ...}) = fold count_literal literals
   5.194  
   5.195 -fun count_user_clause user_lemmas (HOLClause {axiom_name, literals, ...}) =
   5.196 -  member (op =) user_lemmas axiom_name ? fold count_literal literals
   5.197 -
   5.198  fun cnf_helper_thms thy = cnf_rules_pairs thy o map (`Thm.get_name_hint)
   5.199  
   5.200 -fun get_helper_clauses dfg thy isFO (conjectures, axcls, user_lemmas) =
   5.201 +fun get_helper_clauses dfg thy isFO conjectures axcls =
   5.202    if isFO then
   5.203      []
   5.204    else
   5.205      let
   5.206 -        val axclauses = map #2 (make_axiom_clauses dfg thy axcls)
   5.207 -        val ct = init_counters |> fold count_clause conjectures
   5.208 -                               |> fold (count_user_clause user_lemmas) axclauses
   5.209 +        val axclauses = map snd (make_axiom_clauses dfg thy axcls)
   5.210 +        val ct = init_counters
   5.211 +                 |> fold (fold count_clause) [conjectures, axclauses]
   5.212          fun needed c = the (Symtab.lookup ct c) > 0
   5.213          val IK = if needed "c_COMBI" orelse needed "c_COMBK"
   5.214                   then cnf_helper_thms thy [@{thm COMBI_def}, @{thm COMBK_def}]
   5.215 @@ -439,9 +506,7 @@
   5.216                  else []
   5.217          val other = cnf_helper_thms thy [@{thm fequal_imp_equal},
   5.218                                           @{thm equal_imp_fequal}]
   5.219 -    in
   5.220 -        map #2 (make_axiom_clauses dfg thy (other @ IK @ BC @ S))
   5.221 -    end;
   5.222 +    in map snd (make_axiom_clauses dfg thy (other @ IK @ BC @ S)) end
   5.223  
   5.224  (*Find the minimal arity of each function mentioned in the term. Also, note which uses
   5.225    are not at top level, to see if hBOOL is needed.*)
     6.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML	Fri Jun 11 17:07:27 2010 +0200
     6.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML	Fri Jun 11 17:10:23 2010 +0200
     6.3 @@ -345,8 +345,8 @@
     6.4                                >> merge_relevance_overrides))
     6.5                  (add_to_relevance_override [])
     6.6  val parse_sledgehammer_command =
     6.7 -  (Scan.optional Parse.short_ident runN -- parse_params -- parse_relevance_override
     6.8 -   -- Scan.option Parse.nat) #>> sledgehammer_trans
     6.9 +  (Scan.optional Parse.short_ident runN -- parse_params
    6.10 +   -- parse_relevance_override -- Scan.option Parse.nat) #>> sledgehammer_trans
    6.11  val parse_sledgehammer_params_command =
    6.12    parse_params #>> sledgehammer_params_trans
    6.13  
     7.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_proof_reconstruct.ML	Fri Jun 11 17:07:27 2010 +0200
     7.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_proof_reconstruct.ML	Fri Jun 11 17:10:23 2010 +0200
     7.3 @@ -41,12 +41,6 @@
     7.4  fun is_ident_char c = Char.isAlphaNum c orelse c = #"_"
     7.5  fun is_head_digit s = Char.isDigit (String.sub (s, 0))
     7.6  
     7.7 -(* Hack: Could return false positives (e.g., a user happens to declare a
     7.8 -   constant called "SomeTheory.sko_means_shoe_in_$wedish". *)
     7.9 -val is_skolem_const_name =
    7.10 -  Long_Name.base_name
    7.11 -  #> String.isPrefix skolem_prefix andf String.isSubstring skolem_infix
    7.12 -
    7.13  val index_in_shape : int -> int list list -> int =
    7.14    find_index o exists o curry (op =)
    7.15  fun is_axiom_clause_number thm_names num = num <= Vector.length thm_names
    7.16 @@ -263,9 +257,16 @@
    7.17  
    7.18  fun invert_const c = c |> Symtab.lookup const_trans_table_inv |> the_default c
    7.19  
    7.20 -(*The number of type arguments of a constant, zero if it's monomorphic*)
    7.21 +(* The number of type arguments of a constant, zero if it's monomorphic. For
    7.22 +   (instances of) Skolem pseudoconstants, this information is encoded in the
    7.23 +   constant name. *)
    7.24  fun num_type_args thy s =
    7.25 -  length (Sign.const_typargs thy (s, Sign.the_const_type thy s))
    7.26 +  if String.isPrefix skolem_Eps_pseudo_theory s then
    7.27 +    s |> unprefix skolem_Eps_pseudo_theory
    7.28 +      |> space_explode skolem_infix |> hd
    7.29 +      |> space_explode "_" |> List.last |> Int.fromString |> the
    7.30 +  else
    7.31 +    (s, Sign.the_const_type thy s) |> Sign.const_typargs thy |> length
    7.32  
    7.33  fun fix_atp_variable_name s =
    7.34    let
    7.35 @@ -323,9 +324,12 @@
    7.36                          else
    7.37                            (* Extra args from "hAPP" come after any arguments
    7.38                               given directly to the constant. *)
    7.39 -                          Sign.const_instance thy (c,
    7.40 -                                    map (type_from_node tfrees)
    7.41 -                                        (drop num_term_args us)))
    7.42 +                          if String.isPrefix skolem_Eps_pseudo_theory c then
    7.43 +                            map fastype_of ts ---> HOLogic.typeT
    7.44 +                          else
    7.45 +                            Sign.const_instance thy (c,
    7.46 +                                map (type_from_node tfrees)
    7.47 +                                    (drop num_term_args us)))
    7.48            in list_comb (t, ts) end
    7.49          | NONE => (* a free or schematic variable *)
    7.50            let
    7.51 @@ -580,16 +584,29 @@
    7.52        | extract_num (num :: "0" :: "Inp" :: _) = Int.fromString num
    7.53        | extract_num _ = NONE
    7.54    in atp_proof |> split_lines |> map_filter (extract_num o tokens_of) end
    7.55 -  
    7.56 -fun apply_command _ 1 = "by "
    7.57 -  | apply_command 1 _ = "apply "
    7.58 -  | apply_command i _ = "prefer " ^ string_of_int i ^ " apply "
    7.59 -fun metis_command i n [] = apply_command i n ^ "metis"
    7.60 -  | metis_command i n ss =
    7.61 -    apply_command i n ^ "(metis " ^ space_implode " " ss ^ ")"
    7.62 -fun metis_line i n xs =
    7.63 +
    7.64 +val indent_size = 2
    7.65 +val no_label = ("", ~1)
    7.66 +
    7.67 +val raw_prefix = "X"
    7.68 +val assum_prefix = "A"
    7.69 +val fact_prefix = "F"
    7.70 +
    7.71 +fun string_for_label (s, num) = s ^ string_of_int num
    7.72 +
    7.73 +fun metis_using [] = ""
    7.74 +  | metis_using ls =
    7.75 +    "using " ^ space_implode " " (map string_for_label ls) ^ " "
    7.76 +fun metis_apply _ 1 = "by "
    7.77 +  | metis_apply 1 _ = "apply "
    7.78 +  | metis_apply i _ = "prefer " ^ string_of_int i ^ " apply "
    7.79 +fun metis_itself [] = "metis"
    7.80 +  | metis_itself ss = "(metis " ^ space_implode " " ss ^ ")"
    7.81 +fun metis_command i n (ls, ss) =
    7.82 +  metis_using ls ^ metis_apply i n ^ metis_itself ss
    7.83 +fun metis_line i n ss =
    7.84    "Try this command: " ^
    7.85 -  Markup.markup Markup.sendback (metis_command i n xs) ^ ".\n" 
    7.86 +  Markup.markup Markup.sendback (metis_command i n ([], ss)) ^ ".\n"
    7.87  fun minimize_line _ [] = ""
    7.88    | minimize_line minimize_command facts =
    7.89      case minimize_command facts of
    7.90 @@ -639,15 +656,6 @@
    7.91  fun smart_case_split [] facts = ByMetis facts
    7.92    | smart_case_split proofs facts = CaseSplit (proofs, facts)
    7.93  
    7.94 -val indent_size = 2
    7.95 -val no_label = ("", ~1)
    7.96 -
    7.97 -val raw_prefix = "X"
    7.98 -val assum_prefix = "A"
    7.99 -val fact_prefix = "F"
   7.100 -
   7.101 -fun string_for_label (s, num) = s ^ string_of_int num
   7.102 -
   7.103  fun add_fact_from_dep thm_names num =
   7.104    if is_axiom_clause_number thm_names num then
   7.105      apsnd (insert (op =) (Vector.sub (thm_names, num - 1)))
   7.106 @@ -948,7 +956,7 @@
   7.107        let
   7.108          val ls = ls |> sort_distinct (prod_ord string_ord int_ord)
   7.109          val ss = ss |> map unprefix_chained |> sort_distinct string_ord
   7.110 -      in metis_command 1 1 (map string_for_label ls @ ss) end
   7.111 +      in metis_command 1 1 (ls, ss) end
   7.112      and do_step ind (Fix xs) =
   7.113          do_indent ind ^ "fix " ^ space_implode " and " (map do_free xs) ^ "\n"
   7.114        | do_step ind (Let (t1, t2)) =