src/HOL/Tools/metis_tools.ML
changeset 32956 c39860141415
parent 32955 4a78daeb012b
child 32994 ccc07fbbfefd
     1.1 --- a/src/HOL/Tools/metis_tools.ML	Fri Oct 16 10:45:10 2009 +0200
     1.2 +++ b/src/HOL/Tools/metis_tools.ML	Fri Oct 16 10:55:07 2009 +0200
     1.3 @@ -18,728 +18,728 @@
     1.4  structure MetisTools: METIS_TOOLS =
     1.5  struct
     1.6  
     1.7 -  val trace = Unsynchronized.ref false;
     1.8 -  fun trace_msg msg = if ! trace then tracing (msg ()) else ();
     1.9 +val trace = Unsynchronized.ref false;
    1.10 +fun trace_msg msg = if ! trace then tracing (msg ()) else ();
    1.11  
    1.12 -  structure Recon = ResReconstruct;
    1.13 +structure Recon = ResReconstruct;
    1.14  
    1.15 -  val (type_lits, type_lits_setup) = Attrib.config_bool "metis_type_lits" true;
    1.16 +val (type_lits, type_lits_setup) = Attrib.config_bool "metis_type_lits" true;
    1.17  
    1.18 -  datatype mode = FO | HO | FT  (*first-order, higher-order, fully-typed*)
    1.19 +datatype mode = FO | HO | FT  (*first-order, higher-order, fully-typed*)
    1.20  
    1.21 -  (* ------------------------------------------------------------------------- *)
    1.22 -  (* Useful Theorems                                                           *)
    1.23 -  (* ------------------------------------------------------------------------- *)
    1.24 -  val EXCLUDED_MIDDLE = rotate_prems 1 (read_instantiate @{context} [(("R", 0), "False")] notE);
    1.25 -  val REFL_THM = incr_indexes 2 (Meson.make_meta_clause refl);  (*Rename from 0,1*)
    1.26 -  val subst_em  = zero_var_indexes (subst RS EXCLUDED_MIDDLE);
    1.27 -  val ssubst_em = read_instantiate @{context} [(("t", 0), "?s"), (("s", 0), "?t")] (sym RS subst_em);
    1.28 +(* ------------------------------------------------------------------------- *)
    1.29 +(* Useful Theorems                                                           *)
    1.30 +(* ------------------------------------------------------------------------- *)
    1.31 +val EXCLUDED_MIDDLE = rotate_prems 1 (read_instantiate @{context} [(("R", 0), "False")] notE);
    1.32 +val REFL_THM = incr_indexes 2 (Meson.make_meta_clause refl);  (*Rename from 0,1*)
    1.33 +val subst_em  = zero_var_indexes (subst RS EXCLUDED_MIDDLE);
    1.34 +val ssubst_em = read_instantiate @{context} [(("t", 0), "?s"), (("s", 0), "?t")] (sym RS subst_em);
    1.35  
    1.36 -  (* ------------------------------------------------------------------------- *)
    1.37 -  (* Useful Functions                                                          *)
    1.38 -  (* ------------------------------------------------------------------------- *)
    1.39 +(* ------------------------------------------------------------------------- *)
    1.40 +(* Useful Functions                                                          *)
    1.41 +(* ------------------------------------------------------------------------- *)
    1.42  
    1.43 -  (* match untyped terms*)
    1.44 -  fun untyped_aconv (Const(a,_))   (Const(b,_))   = (a=b)
    1.45 -    | untyped_aconv (Free(a,_))    (Free(b,_))    = (a=b)
    1.46 -    | untyped_aconv (Var((a,_),_)) (Var((b,_),_)) = (a=b)   (*the index is ignored!*)
    1.47 -    | untyped_aconv (Bound i)      (Bound j)      = (i=j)
    1.48 -    | untyped_aconv (Abs(a,_,t))  (Abs(b,_,u))    = (a=b) andalso untyped_aconv t u
    1.49 -    | untyped_aconv (t1$t2) (u1$u2)  = untyped_aconv t1 u1 andalso untyped_aconv t2 u2
    1.50 -    | untyped_aconv _              _              = false;
    1.51 +(* match untyped terms*)
    1.52 +fun untyped_aconv (Const(a,_))   (Const(b,_))   = (a=b)
    1.53 +  | untyped_aconv (Free(a,_))    (Free(b,_))    = (a=b)
    1.54 +  | untyped_aconv (Var((a,_),_)) (Var((b,_),_)) = (a=b)   (*the index is ignored!*)
    1.55 +  | untyped_aconv (Bound i)      (Bound j)      = (i=j)
    1.56 +  | untyped_aconv (Abs(a,_,t))  (Abs(b,_,u))    = (a=b) andalso untyped_aconv t u
    1.57 +  | untyped_aconv (t1$t2) (u1$u2)  = untyped_aconv t1 u1 andalso untyped_aconv t2 u2
    1.58 +  | untyped_aconv _              _              = false;
    1.59  
    1.60 -  (* Finding the relative location of an untyped term within a list of terms *)
    1.61 -  fun get_index lit =
    1.62 -    let val lit = Envir.eta_contract lit
    1.63 -        fun get n [] = raise Empty
    1.64 -          | get n (x::xs) = if untyped_aconv lit (Envir.eta_contract (HOLogic.dest_Trueprop x))
    1.65 -                            then n  else get (n+1) xs
    1.66 -    in get 1 end;
    1.67 +(* Finding the relative location of an untyped term within a list of terms *)
    1.68 +fun get_index lit =
    1.69 +  let val lit = Envir.eta_contract lit
    1.70 +      fun get n [] = raise Empty
    1.71 +        | get n (x::xs) = if untyped_aconv lit (Envir.eta_contract (HOLogic.dest_Trueprop x))
    1.72 +                          then n  else get (n+1) xs
    1.73 +  in get 1 end;
    1.74  
    1.75 -  (* ------------------------------------------------------------------------- *)
    1.76 -  (* HOL to FOL  (Isabelle to Metis)                                           *)
    1.77 -  (* ------------------------------------------------------------------------- *)
    1.78 +(* ------------------------------------------------------------------------- *)
    1.79 +(* HOL to FOL  (Isabelle to Metis)                                           *)
    1.80 +(* ------------------------------------------------------------------------- *)
    1.81  
    1.82 -  fun fn_isa_to_met "equal" = "="
    1.83 -    | fn_isa_to_met x       = x;
    1.84 +fun fn_isa_to_met "equal" = "="
    1.85 +  | fn_isa_to_met x       = x;
    1.86  
    1.87 -  fun metis_lit b c args = (b, (c, args));
    1.88 +fun metis_lit b c args = (b, (c, args));
    1.89  
    1.90 -  fun hol_type_to_fol (ResClause.AtomV x) = Metis.Term.Var x
    1.91 -    | hol_type_to_fol (ResClause.AtomF x) = Metis.Term.Fn(x,[])
    1.92 -    | hol_type_to_fol (ResClause.Comp(tc,tps)) = Metis.Term.Fn(tc, map hol_type_to_fol tps);
    1.93 +fun hol_type_to_fol (ResClause.AtomV x) = Metis.Term.Var x
    1.94 +  | hol_type_to_fol (ResClause.AtomF x) = Metis.Term.Fn(x,[])
    1.95 +  | hol_type_to_fol (ResClause.Comp(tc,tps)) = Metis.Term.Fn(tc, map hol_type_to_fol tps);
    1.96  
    1.97 -  (*These two functions insert type literals before the real literals. That is the
    1.98 -    opposite order from TPTP linkup, but maybe OK.*)
    1.99 +(*These two functions insert type literals before the real literals. That is the
   1.100 +  opposite order from TPTP linkup, but maybe OK.*)
   1.101  
   1.102 -  fun hol_term_to_fol_FO tm =
   1.103 -    case ResHolClause.strip_comb tm of
   1.104 -        (ResHolClause.CombConst(c,_,tys), tms) =>
   1.105 -          let val tyargs = map hol_type_to_fol tys
   1.106 -              val args   = map hol_term_to_fol_FO tms
   1.107 -          in Metis.Term.Fn (c, tyargs @ args) end
   1.108 -      | (ResHolClause.CombVar(v,_), []) => Metis.Term.Var v
   1.109 -      | _ => error "hol_term_to_fol_FO";
   1.110 +fun hol_term_to_fol_FO tm =
   1.111 +  case ResHolClause.strip_comb tm of
   1.112 +      (ResHolClause.CombConst(c,_,tys), tms) =>
   1.113 +        let val tyargs = map hol_type_to_fol tys
   1.114 +            val args   = map hol_term_to_fol_FO tms
   1.115 +        in Metis.Term.Fn (c, tyargs @ args) end
   1.116 +    | (ResHolClause.CombVar(v,_), []) => Metis.Term.Var v
   1.117 +    | _ => error "hol_term_to_fol_FO";
   1.118  
   1.119 -  fun hol_term_to_fol_HO (ResHolClause.CombVar(a, ty)) = Metis.Term.Var a
   1.120 -    | hol_term_to_fol_HO (ResHolClause.CombConst(a, ty, tylist)) =
   1.121 -        Metis.Term.Fn(fn_isa_to_met a, map hol_type_to_fol tylist)
   1.122 -    | hol_term_to_fol_HO (ResHolClause.CombApp(tm1,tm2)) =
   1.123 -         Metis.Term.Fn(".", map hol_term_to_fol_HO [tm1,tm2]);
   1.124 +fun hol_term_to_fol_HO (ResHolClause.CombVar(a, ty)) = Metis.Term.Var a
   1.125 +  | hol_term_to_fol_HO (ResHolClause.CombConst(a, ty, tylist)) =
   1.126 +      Metis.Term.Fn(fn_isa_to_met a, map hol_type_to_fol tylist)
   1.127 +  | hol_term_to_fol_HO (ResHolClause.CombApp(tm1,tm2)) =
   1.128 +       Metis.Term.Fn(".", map hol_term_to_fol_HO [tm1,tm2]);
   1.129  
   1.130 -  (*The fully-typed translation, to avoid type errors*)
   1.131 -  fun wrap_type (tm, ty) = Metis.Term.Fn("ti", [tm, hol_type_to_fol ty]);
   1.132 -  
   1.133 -  fun hol_term_to_fol_FT (ResHolClause.CombVar(a, ty)) = 
   1.134 -        wrap_type (Metis.Term.Var a, ty)
   1.135 -    | hol_term_to_fol_FT (ResHolClause.CombConst(a, ty, _)) =
   1.136 -        wrap_type (Metis.Term.Fn(fn_isa_to_met a, []), ty)
   1.137 -    | hol_term_to_fol_FT (tm as ResHolClause.CombApp(tm1,tm2)) =
   1.138 -         wrap_type (Metis.Term.Fn(".", map hol_term_to_fol_FT [tm1,tm2]),    
   1.139 -                    ResHolClause.type_of_combterm tm);
   1.140 +(*The fully-typed translation, to avoid type errors*)
   1.141 +fun wrap_type (tm, ty) = Metis.Term.Fn("ti", [tm, hol_type_to_fol ty]);
   1.142 +
   1.143 +fun hol_term_to_fol_FT (ResHolClause.CombVar(a, ty)) =
   1.144 +      wrap_type (Metis.Term.Var a, ty)
   1.145 +  | hol_term_to_fol_FT (ResHolClause.CombConst(a, ty, _)) =
   1.146 +      wrap_type (Metis.Term.Fn(fn_isa_to_met a, []), ty)
   1.147 +  | hol_term_to_fol_FT (tm as ResHolClause.CombApp(tm1,tm2)) =
   1.148 +       wrap_type (Metis.Term.Fn(".", map hol_term_to_fol_FT [tm1,tm2]),
   1.149 +                  ResHolClause.type_of_combterm tm);
   1.150  
   1.151 -  fun hol_literal_to_fol FO (ResHolClause.Literal (pol, tm)) =  
   1.152 -        let val (ResHolClause.CombConst(p,_,tys), tms) = ResHolClause.strip_comb tm
   1.153 -            val tylits = if p = "equal" then [] else map hol_type_to_fol tys
   1.154 -            val lits = map hol_term_to_fol_FO tms
   1.155 -        in metis_lit pol (fn_isa_to_met p) (tylits @ lits) end
   1.156 -    | hol_literal_to_fol HO (ResHolClause.Literal (pol, tm)) =
   1.157 -       (case ResHolClause.strip_comb tm of
   1.158 -            (ResHolClause.CombConst("equal",_,_), tms) =>
   1.159 -              metis_lit pol "=" (map hol_term_to_fol_HO tms)
   1.160 -          | _ => metis_lit pol "{}" [hol_term_to_fol_HO tm])   (*hBOOL*)
   1.161 -    | hol_literal_to_fol FT (ResHolClause.Literal (pol, tm)) = 
   1.162 -       (case ResHolClause.strip_comb tm of
   1.163 -            (ResHolClause.CombConst("equal",_,_), tms) =>
   1.164 -              metis_lit pol "=" (map hol_term_to_fol_FT tms)
   1.165 -          | _ => metis_lit pol "{}" [hol_term_to_fol_FT tm])   (*hBOOL*);
   1.166 +fun hol_literal_to_fol FO (ResHolClause.Literal (pol, tm)) =
   1.167 +      let val (ResHolClause.CombConst(p,_,tys), tms) = ResHolClause.strip_comb tm
   1.168 +          val tylits = if p = "equal" then [] else map hol_type_to_fol tys
   1.169 +          val lits = map hol_term_to_fol_FO tms
   1.170 +      in metis_lit pol (fn_isa_to_met p) (tylits @ lits) end
   1.171 +  | hol_literal_to_fol HO (ResHolClause.Literal (pol, tm)) =
   1.172 +     (case ResHolClause.strip_comb tm of
   1.173 +          (ResHolClause.CombConst("equal",_,_), tms) =>
   1.174 +            metis_lit pol "=" (map hol_term_to_fol_HO tms)
   1.175 +        | _ => metis_lit pol "{}" [hol_term_to_fol_HO tm])   (*hBOOL*)
   1.176 +  | hol_literal_to_fol FT (ResHolClause.Literal (pol, tm)) =
   1.177 +     (case ResHolClause.strip_comb tm of
   1.178 +          (ResHolClause.CombConst("equal",_,_), tms) =>
   1.179 +            metis_lit pol "=" (map hol_term_to_fol_FT tms)
   1.180 +        | _ => metis_lit pol "{}" [hol_term_to_fol_FT tm])   (*hBOOL*);
   1.181  
   1.182 -  fun literals_of_hol_thm thy mode t =
   1.183 -        let val (lits, types_sorts) = ResHolClause.literals_of_term thy t
   1.184 -        in  (map (hol_literal_to_fol mode) lits, types_sorts) end;
   1.185 +fun literals_of_hol_thm thy mode t =
   1.186 +      let val (lits, types_sorts) = ResHolClause.literals_of_term thy t
   1.187 +      in  (map (hol_literal_to_fol mode) lits, types_sorts) end;
   1.188  
   1.189 -  (*Sign should be "true" for conjecture type constraints, "false" for type lits in clauses.*)
   1.190 -  fun metis_of_typeLit pos (ResClause.LTVar (s,x))  = metis_lit pos s [Metis.Term.Var x]
   1.191 -    | metis_of_typeLit pos (ResClause.LTFree (s,x)) = metis_lit pos s [Metis.Term.Fn(x,[])];
   1.192 +(*Sign should be "true" for conjecture type constraints, "false" for type lits in clauses.*)
   1.193 +fun metis_of_typeLit pos (ResClause.LTVar (s,x))  = metis_lit pos s [Metis.Term.Var x]
   1.194 +  | metis_of_typeLit pos (ResClause.LTFree (s,x)) = metis_lit pos s [Metis.Term.Fn(x,[])];
   1.195  
   1.196 -  fun default_sort ctxt (TVar _) = false
   1.197 -    | default_sort ctxt (TFree(x,s)) = (s = Option.getOpt (Variable.def_sort ctxt (x,~1), []));
   1.198 +fun default_sort ctxt (TVar _) = false
   1.199 +  | default_sort ctxt (TFree(x,s)) = (s = Option.getOpt (Variable.def_sort ctxt (x,~1), []));
   1.200  
   1.201 -  fun metis_of_tfree tf =
   1.202 -    Metis.Thm.axiom (Metis.LiteralSet.singleton (metis_of_typeLit true tf));
   1.203 +fun metis_of_tfree tf =
   1.204 +  Metis.Thm.axiom (Metis.LiteralSet.singleton (metis_of_typeLit true tf));
   1.205  
   1.206 -  fun hol_thm_to_fol is_conjecture ctxt mode th =
   1.207 -    let val thy = ProofContext.theory_of ctxt
   1.208 -        val (mlits, types_sorts) =
   1.209 -               (literals_of_hol_thm thy mode o HOLogic.dest_Trueprop o prop_of) th
   1.210 -    in
   1.211 -        if is_conjecture then
   1.212 -            (Metis.Thm.axiom (Metis.LiteralSet.fromList mlits), ResClause.add_typs types_sorts)
   1.213 -        else
   1.214 -          let val tylits = ResClause.add_typs
   1.215 -                             (filter (not o default_sort ctxt) types_sorts)
   1.216 -              val mtylits = if Config.get ctxt type_lits
   1.217 -                            then map (metis_of_typeLit false) tylits else []
   1.218 -          in
   1.219 -            (Metis.Thm.axiom (Metis.LiteralSet.fromList(mtylits @ mlits)), [])
   1.220 -          end
   1.221 -    end;
   1.222 +fun hol_thm_to_fol is_conjecture ctxt mode th =
   1.223 +  let val thy = ProofContext.theory_of ctxt
   1.224 +      val (mlits, types_sorts) =
   1.225 +             (literals_of_hol_thm thy mode o HOLogic.dest_Trueprop o prop_of) th
   1.226 +  in
   1.227 +      if is_conjecture then
   1.228 +          (Metis.Thm.axiom (Metis.LiteralSet.fromList mlits), ResClause.add_typs types_sorts)
   1.229 +      else
   1.230 +        let val tylits = ResClause.add_typs
   1.231 +                           (filter (not o default_sort ctxt) types_sorts)
   1.232 +            val mtylits = if Config.get ctxt type_lits
   1.233 +                          then map (metis_of_typeLit false) tylits else []
   1.234 +        in
   1.235 +          (Metis.Thm.axiom (Metis.LiteralSet.fromList(mtylits @ mlits)), [])
   1.236 +        end
   1.237 +  end;
   1.238  
   1.239 -  (* ARITY CLAUSE *)
   1.240 +(* ARITY CLAUSE *)
   1.241  
   1.242 -  fun m_arity_cls (ResClause.TConsLit (c,t,args)) =
   1.243 -        metis_lit true (ResClause.make_type_class c) [Metis.Term.Fn(t, map Metis.Term.Var args)]
   1.244 -    | m_arity_cls (ResClause.TVarLit (c,str))     =
   1.245 -        metis_lit false (ResClause.make_type_class c) [Metis.Term.Var str];
   1.246 +fun m_arity_cls (ResClause.TConsLit (c,t,args)) =
   1.247 +      metis_lit true (ResClause.make_type_class c) [Metis.Term.Fn(t, map Metis.Term.Var args)]
   1.248 +  | m_arity_cls (ResClause.TVarLit (c,str))     =
   1.249 +      metis_lit false (ResClause.make_type_class c) [Metis.Term.Var str];
   1.250  
   1.251 -  (*TrueI is returned as the Isabelle counterpart because there isn't any.*)
   1.252 -  fun arity_cls (ResClause.ArityClause{conclLit,premLits,...}) =
   1.253 -    (TrueI,
   1.254 -     Metis.Thm.axiom (Metis.LiteralSet.fromList (map m_arity_cls (conclLit :: premLits))));
   1.255 +(*TrueI is returned as the Isabelle counterpart because there isn't any.*)
   1.256 +fun arity_cls (ResClause.ArityClause{conclLit,premLits,...}) =
   1.257 +  (TrueI,
   1.258 +   Metis.Thm.axiom (Metis.LiteralSet.fromList (map m_arity_cls (conclLit :: premLits))));
   1.259  
   1.260 -  (* CLASSREL CLAUSE *)
   1.261 +(* CLASSREL CLAUSE *)
   1.262  
   1.263 -  fun m_classrel_cls subclass superclass =
   1.264 -    [metis_lit false subclass [Metis.Term.Var "T"], metis_lit true superclass [Metis.Term.Var "T"]];
   1.265 +fun m_classrel_cls subclass superclass =
   1.266 +  [metis_lit false subclass [Metis.Term.Var "T"], metis_lit true superclass [Metis.Term.Var "T"]];
   1.267  
   1.268 -  fun classrel_cls (ResClause.ClassrelClause {axiom_name,subclass,superclass,...}) =
   1.269 -    (TrueI, Metis.Thm.axiom (Metis.LiteralSet.fromList (m_classrel_cls subclass superclass)));
   1.270 +fun classrel_cls (ResClause.ClassrelClause {axiom_name,subclass,superclass,...}) =
   1.271 +  (TrueI, Metis.Thm.axiom (Metis.LiteralSet.fromList (m_classrel_cls subclass superclass)));
   1.272  
   1.273 -  (* ------------------------------------------------------------------------- *)
   1.274 -  (* FOL to HOL  (Metis to Isabelle)                                           *)
   1.275 -  (* ------------------------------------------------------------------------- *)
   1.276 +(* ------------------------------------------------------------------------- *)
   1.277 +(* FOL to HOL  (Metis to Isabelle)                                           *)
   1.278 +(* ------------------------------------------------------------------------- *)
   1.279  
   1.280 - datatype term_or_type = Term of Term.term | Type of Term.typ;
   1.281 +datatype term_or_type = Term of Term.term | Type of Term.typ;
   1.282  
   1.283 -  fun terms_of [] = []
   1.284 -    | terms_of (Term t :: tts) = t :: terms_of tts
   1.285 -    | terms_of (Type _ :: tts) = terms_of tts;
   1.286 +fun terms_of [] = []
   1.287 +  | terms_of (Term t :: tts) = t :: terms_of tts
   1.288 +  | terms_of (Type _ :: tts) = terms_of tts;
   1.289  
   1.290 -  fun types_of [] = []
   1.291 -    | types_of (Term (Term.Var((a,idx), T)) :: tts) =
   1.292 -        if String.isPrefix "_" a then
   1.293 -            (*Variable generated by Metis, which might have been a type variable.*)
   1.294 -            TVar(("'" ^ a, idx), HOLogic.typeS) :: types_of tts
   1.295 -        else types_of tts
   1.296 -    | types_of (Term _ :: tts) = types_of tts
   1.297 -    | types_of (Type T :: tts) = T :: types_of tts;
   1.298 +fun types_of [] = []
   1.299 +  | types_of (Term (Term.Var((a,idx), T)) :: tts) =
   1.300 +      if String.isPrefix "_" a then
   1.301 +          (*Variable generated by Metis, which might have been a type variable.*)
   1.302 +          TVar(("'" ^ a, idx), HOLogic.typeS) :: types_of tts
   1.303 +      else types_of tts
   1.304 +  | types_of (Term _ :: tts) = types_of tts
   1.305 +  | types_of (Type T :: tts) = T :: types_of tts;
   1.306  
   1.307 -  fun apply_list rator nargs rands =
   1.308 -    let val trands = terms_of rands
   1.309 -    in  if length trands = nargs then Term (list_comb(rator, trands))
   1.310 -        else error
   1.311 -          ("apply_list: wrong number of arguments: " ^ Syntax.string_of_term_global Pure.thy rator ^
   1.312 -            " expected " ^ Int.toString nargs ^
   1.313 -            " received " ^ commas (map (Syntax.string_of_term_global Pure.thy) trands))
   1.314 -    end;
   1.315 +fun apply_list rator nargs rands =
   1.316 +  let val trands = terms_of rands
   1.317 +  in  if length trands = nargs then Term (list_comb(rator, trands))
   1.318 +      else error
   1.319 +        ("apply_list: wrong number of arguments: " ^ Syntax.string_of_term_global Pure.thy rator ^
   1.320 +          " expected " ^ Int.toString nargs ^
   1.321 +          " received " ^ commas (map (Syntax.string_of_term_global Pure.thy) trands))
   1.322 +  end;
   1.323  
   1.324  fun infer_types ctxt =
   1.325    Syntax.check_terms (ProofContext.set_mode ProofContext.mode_pattern ctxt);
   1.326  
   1.327 -  (*We use 1 rather than 0 because variable references in clauses may otherwise conflict
   1.328 -    with variable constraints in the goal...at least, type inference often fails otherwise.
   1.329 -    SEE ALSO axiom_inf below.*)
   1.330 -  fun mk_var (w,T) = Term.Var((w,1), T);
   1.331 +(*We use 1 rather than 0 because variable references in clauses may otherwise conflict
   1.332 +  with variable constraints in the goal...at least, type inference often fails otherwise.
   1.333 +  SEE ALSO axiom_inf below.*)
   1.334 +fun mk_var (w,T) = Term.Var((w,1), T);
   1.335  
   1.336 -  (*include the default sort, if available*)
   1.337 -  fun mk_tfree ctxt w =
   1.338 -    let val ww = "'" ^ w
   1.339 -    in  TFree(ww, getOpt (Variable.def_sort ctxt (ww,~1), HOLogic.typeS))  end;
   1.340 +(*include the default sort, if available*)
   1.341 +fun mk_tfree ctxt w =
   1.342 +  let val ww = "'" ^ w
   1.343 +  in  TFree(ww, getOpt (Variable.def_sort ctxt (ww,~1), HOLogic.typeS))  end;
   1.344  
   1.345 -  (*Remove the "apply" operator from an HO term*)
   1.346 -  fun strip_happ args (Metis.Term.Fn(".",[t,u])) = strip_happ (u::args) t
   1.347 -    | strip_happ args x = (x, args);
   1.348 +(*Remove the "apply" operator from an HO term*)
   1.349 +fun strip_happ args (Metis.Term.Fn(".",[t,u])) = strip_happ (u::args) t
   1.350 +  | strip_happ args x = (x, args);
   1.351  
   1.352 -  fun fol_type_to_isa ctxt (Metis.Term.Var v) = 
   1.353 -       (case Recon.strip_prefix ResClause.tvar_prefix v of
   1.354 -	    SOME w => Recon.make_tvar w
   1.355 -	  | NONE   => Recon.make_tvar v)
   1.356 -    | fol_type_to_isa ctxt (Metis.Term.Fn(x, tys)) =
   1.357 -       (case Recon.strip_prefix ResClause.tconst_prefix x of
   1.358 -	    SOME tc => Term.Type (Recon.invert_type_const tc, map (fol_type_to_isa ctxt) tys)
   1.359 -	  | NONE    => 
   1.360 -        case Recon.strip_prefix ResClause.tfree_prefix x of
   1.361 -	    SOME tf => mk_tfree ctxt tf
   1.362 -	  | NONE    => error ("fol_type_to_isa: " ^ x));
   1.363 +fun fol_type_to_isa ctxt (Metis.Term.Var v) =
   1.364 +     (case Recon.strip_prefix ResClause.tvar_prefix v of
   1.365 +          SOME w => Recon.make_tvar w
   1.366 +        | NONE   => Recon.make_tvar v)
   1.367 +  | fol_type_to_isa ctxt (Metis.Term.Fn(x, tys)) =
   1.368 +     (case Recon.strip_prefix ResClause.tconst_prefix x of
   1.369 +          SOME tc => Term.Type (Recon.invert_type_const tc, map (fol_type_to_isa ctxt) tys)
   1.370 +        | NONE    =>
   1.371 +      case Recon.strip_prefix ResClause.tfree_prefix x of
   1.372 +          SOME tf => mk_tfree ctxt tf
   1.373 +        | NONE    => error ("fol_type_to_isa: " ^ x));
   1.374  
   1.375 -  (*Maps metis terms to isabelle terms*)
   1.376 -  fun fol_term_to_hol_RAW ctxt fol_tm =
   1.377 -    let val thy = ProofContext.theory_of ctxt
   1.378 -        val _ = trace_msg (fn () => "fol_term_to_hol: " ^ Metis.Term.toString fol_tm)
   1.379 -        fun tm_to_tt (Metis.Term.Var v) =
   1.380 -               (case Recon.strip_prefix ResClause.tvar_prefix v of
   1.381 -                    SOME w => Type (Recon.make_tvar w)
   1.382 -                  | NONE =>
   1.383 -                case Recon.strip_prefix ResClause.schematic_var_prefix v of
   1.384 -                    SOME w => Term (mk_var (w, HOLogic.typeT))
   1.385 -                  | NONE   => Term (mk_var (v, HOLogic.typeT)) )
   1.386 -                      (*Var from Metis with a name like _nnn; possibly a type variable*)
   1.387 -          | tm_to_tt (Metis.Term.Fn ("{}", [arg])) = tm_to_tt arg   (*hBOOL*)
   1.388 -          | tm_to_tt (t as Metis.Term.Fn (".",_)) =
   1.389 -              let val (rator,rands) = strip_happ [] t
   1.390 -              in  case rator of
   1.391 -                      Metis.Term.Fn(fname,ts) => applic_to_tt (fname, ts @ rands)
   1.392 -                    | _ => case tm_to_tt rator of
   1.393 -                               Term t => Term (list_comb(t, terms_of (map tm_to_tt rands)))
   1.394 -                             | _ => error "tm_to_tt: HO application"
   1.395 -              end
   1.396 -          | tm_to_tt (Metis.Term.Fn (fname, args)) = applic_to_tt (fname,args)
   1.397 -        and applic_to_tt ("=",ts) =
   1.398 -              Term (list_comb(Const ("op =", HOLogic.typeT), terms_of (map tm_to_tt ts)))
   1.399 -          | applic_to_tt (a,ts) =
   1.400 -              case Recon.strip_prefix ResClause.const_prefix a of
   1.401 -                  SOME b =>
   1.402 -                    let val c = Recon.invert_const b
   1.403 -                        val ntypes = Recon.num_typargs thy c
   1.404 -                        val nterms = length ts - ntypes
   1.405 -                        val tts = map tm_to_tt ts
   1.406 -                        val tys = types_of (List.take(tts,ntypes))
   1.407 -                        val ntyargs = Recon.num_typargs thy c
   1.408 -                    in if length tys = ntyargs then
   1.409 -                           apply_list (Const (c, dummyT)) nterms (List.drop(tts,ntypes))
   1.410 -                       else error ("Constant " ^ c ^ " expects " ^ Int.toString ntyargs ^
   1.411 -                                   " but gets " ^ Int.toString (length tys) ^
   1.412 -                                   " type arguments\n" ^
   1.413 -                                   cat_lines (map (Syntax.string_of_typ ctxt) tys) ^
   1.414 -                                   " the terms are \n" ^
   1.415 -                                   cat_lines (map (Syntax.string_of_term ctxt) (terms_of tts)))
   1.416 -                       end
   1.417 -                | NONE => (*Not a constant. Is it a type constructor?*)
   1.418 -              case Recon.strip_prefix ResClause.tconst_prefix a of
   1.419 -                  SOME b => Type (Term.Type(Recon.invert_type_const b, types_of (map tm_to_tt ts)))
   1.420 -                | NONE => (*Maybe a TFree. Should then check that ts=[].*)
   1.421 -              case Recon.strip_prefix ResClause.tfree_prefix a of
   1.422 -                  SOME b => Type (mk_tfree ctxt b)
   1.423 -                | NONE => (*a fixed variable? They are Skolem functions.*)
   1.424 -              case Recon.strip_prefix ResClause.fixed_var_prefix a of
   1.425 -                  SOME b =>
   1.426 -                    let val opr = Term.Free(b, HOLogic.typeT)
   1.427 -                    in  apply_list opr (length ts) (map tm_to_tt ts)  end
   1.428 -                | NONE => error ("unexpected metis function: " ^ a)
   1.429 -    in  case tm_to_tt fol_tm of Term t => t | _ => error "fol_tm_to_tt: Term expected"  end;
   1.430 +(*Maps metis terms to isabelle terms*)
   1.431 +fun fol_term_to_hol_RAW ctxt fol_tm =
   1.432 +  let val thy = ProofContext.theory_of ctxt
   1.433 +      val _ = trace_msg (fn () => "fol_term_to_hol: " ^ Metis.Term.toString fol_tm)
   1.434 +      fun tm_to_tt (Metis.Term.Var v) =
   1.435 +             (case Recon.strip_prefix ResClause.tvar_prefix v of
   1.436 +                  SOME w => Type (Recon.make_tvar w)
   1.437 +                | NONE =>
   1.438 +              case Recon.strip_prefix ResClause.schematic_var_prefix v of
   1.439 +                  SOME w => Term (mk_var (w, HOLogic.typeT))
   1.440 +                | NONE   => Term (mk_var (v, HOLogic.typeT)) )
   1.441 +                    (*Var from Metis with a name like _nnn; possibly a type variable*)
   1.442 +        | tm_to_tt (Metis.Term.Fn ("{}", [arg])) = tm_to_tt arg   (*hBOOL*)
   1.443 +        | tm_to_tt (t as Metis.Term.Fn (".",_)) =
   1.444 +            let val (rator,rands) = strip_happ [] t
   1.445 +            in  case rator of
   1.446 +                    Metis.Term.Fn(fname,ts) => applic_to_tt (fname, ts @ rands)
   1.447 +                  | _ => case tm_to_tt rator of
   1.448 +                             Term t => Term (list_comb(t, terms_of (map tm_to_tt rands)))
   1.449 +                           | _ => error "tm_to_tt: HO application"
   1.450 +            end
   1.451 +        | tm_to_tt (Metis.Term.Fn (fname, args)) = applic_to_tt (fname,args)
   1.452 +      and applic_to_tt ("=",ts) =
   1.453 +            Term (list_comb(Const ("op =", HOLogic.typeT), terms_of (map tm_to_tt ts)))
   1.454 +        | applic_to_tt (a,ts) =
   1.455 +            case Recon.strip_prefix ResClause.const_prefix a of
   1.456 +                SOME b =>
   1.457 +                  let val c = Recon.invert_const b
   1.458 +                      val ntypes = Recon.num_typargs thy c
   1.459 +                      val nterms = length ts - ntypes
   1.460 +                      val tts = map tm_to_tt ts
   1.461 +                      val tys = types_of (List.take(tts,ntypes))
   1.462 +                      val ntyargs = Recon.num_typargs thy c
   1.463 +                  in if length tys = ntyargs then
   1.464 +                         apply_list (Const (c, dummyT)) nterms (List.drop(tts,ntypes))
   1.465 +                     else error ("Constant " ^ c ^ " expects " ^ Int.toString ntyargs ^
   1.466 +                                 " but gets " ^ Int.toString (length tys) ^
   1.467 +                                 " type arguments\n" ^
   1.468 +                                 cat_lines (map (Syntax.string_of_typ ctxt) tys) ^
   1.469 +                                 " the terms are \n" ^
   1.470 +                                 cat_lines (map (Syntax.string_of_term ctxt) (terms_of tts)))
   1.471 +                     end
   1.472 +              | NONE => (*Not a constant. Is it a type constructor?*)
   1.473 +            case Recon.strip_prefix ResClause.tconst_prefix a of
   1.474 +                SOME b => Type (Term.Type(Recon.invert_type_const b, types_of (map tm_to_tt ts)))
   1.475 +              | NONE => (*Maybe a TFree. Should then check that ts=[].*)
   1.476 +            case Recon.strip_prefix ResClause.tfree_prefix a of
   1.477 +                SOME b => Type (mk_tfree ctxt b)
   1.478 +              | NONE => (*a fixed variable? They are Skolem functions.*)
   1.479 +            case Recon.strip_prefix ResClause.fixed_var_prefix a of
   1.480 +                SOME b =>
   1.481 +                  let val opr = Term.Free(b, HOLogic.typeT)
   1.482 +                  in  apply_list opr (length ts) (map tm_to_tt ts)  end
   1.483 +              | NONE => error ("unexpected metis function: " ^ a)
   1.484 +  in  case tm_to_tt fol_tm of Term t => t | _ => error "fol_tm_to_tt: Term expected"  end;
   1.485  
   1.486 -  (*Maps fully-typed metis terms to isabelle terms*)
   1.487 -  fun fol_term_to_hol_FT ctxt fol_tm =
   1.488 -    let val _ = trace_msg (fn () => "fol_term_to_hol_FT: " ^ Metis.Term.toString fol_tm)
   1.489 -        fun cvt (Metis.Term.Fn ("ti", [Metis.Term.Var v, ty])) =
   1.490 -               (case Recon.strip_prefix ResClause.schematic_var_prefix v of
   1.491 -                    SOME w =>  mk_var(w, dummyT)
   1.492 -                  | NONE   => mk_var(v, dummyT))
   1.493 -          | cvt (Metis.Term.Fn ("ti", [Metis.Term.Fn ("=",[]), ty])) = 
   1.494 -              Const ("op =", HOLogic.typeT)
   1.495 -          | cvt (Metis.Term.Fn ("ti", [Metis.Term.Fn (x,[]), ty])) =
   1.496 -             (case Recon.strip_prefix ResClause.const_prefix x of
   1.497 -                  SOME c => Const (Recon.invert_const c, dummyT)
   1.498 -                | NONE => (*Not a constant. Is it a fixed variable??*)
   1.499 -              case Recon.strip_prefix ResClause.fixed_var_prefix x of
   1.500 -                  SOME v => Free (v, fol_type_to_isa ctxt ty)
   1.501 -                | NONE => error ("fol_term_to_hol_FT bad constant: " ^ x))
   1.502 -          | cvt (Metis.Term.Fn ("ti", [Metis.Term.Fn (".",[tm1,tm2]), _])) =
   1.503 -              cvt tm1 $ cvt tm2
   1.504 -          | cvt (Metis.Term.Fn (".",[tm1,tm2])) = (*untyped application*)
   1.505 -              cvt tm1 $ cvt tm2
   1.506 -          | cvt (Metis.Term.Fn ("{}", [arg])) = cvt arg   (*hBOOL*)
   1.507 -          | cvt (Metis.Term.Fn ("=", [tm1,tm2])) = 
   1.508 -              list_comb(Const ("op =", HOLogic.typeT), map cvt [tm1,tm2])
   1.509 -          | cvt (t as Metis.Term.Fn (x, [])) = 
   1.510 -             (case Recon.strip_prefix ResClause.const_prefix x of
   1.511 -                  SOME c => Const (Recon.invert_const c, dummyT)
   1.512 -                | NONE => (*Not a constant. Is it a fixed variable??*)
   1.513 -              case Recon.strip_prefix ResClause.fixed_var_prefix x of
   1.514 -                  SOME v => Free (v, dummyT)
   1.515 -                | NONE =>  (trace_msg (fn () => "fol_term_to_hol_FT bad const: " ^ x); fol_term_to_hol_RAW ctxt t))
   1.516 -          | cvt t = (trace_msg (fn () => "fol_term_to_hol_FT bad term: " ^ Metis.Term.toString t); fol_term_to_hol_RAW ctxt t)
   1.517 -    in  cvt fol_tm   end;
   1.518 +(*Maps fully-typed metis terms to isabelle terms*)
   1.519 +fun fol_term_to_hol_FT ctxt fol_tm =
   1.520 +  let val _ = trace_msg (fn () => "fol_term_to_hol_FT: " ^ Metis.Term.toString fol_tm)
   1.521 +      fun cvt (Metis.Term.Fn ("ti", [Metis.Term.Var v, ty])) =
   1.522 +             (case Recon.strip_prefix ResClause.schematic_var_prefix v of
   1.523 +                  SOME w =>  mk_var(w, dummyT)
   1.524 +                | NONE   => mk_var(v, dummyT))
   1.525 +        | cvt (Metis.Term.Fn ("ti", [Metis.Term.Fn ("=",[]), ty])) =
   1.526 +            Const ("op =", HOLogic.typeT)
   1.527 +        | cvt (Metis.Term.Fn ("ti", [Metis.Term.Fn (x,[]), ty])) =
   1.528 +           (case Recon.strip_prefix ResClause.const_prefix x of
   1.529 +                SOME c => Const (Recon.invert_const c, dummyT)
   1.530 +              | NONE => (*Not a constant. Is it a fixed variable??*)
   1.531 +            case Recon.strip_prefix ResClause.fixed_var_prefix x of
   1.532 +                SOME v => Free (v, fol_type_to_isa ctxt ty)
   1.533 +              | NONE => error ("fol_term_to_hol_FT bad constant: " ^ x))
   1.534 +        | cvt (Metis.Term.Fn ("ti", [Metis.Term.Fn (".",[tm1,tm2]), _])) =
   1.535 +            cvt tm1 $ cvt tm2
   1.536 +        | cvt (Metis.Term.Fn (".",[tm1,tm2])) = (*untyped application*)
   1.537 +            cvt tm1 $ cvt tm2
   1.538 +        | cvt (Metis.Term.Fn ("{}", [arg])) = cvt arg   (*hBOOL*)
   1.539 +        | cvt (Metis.Term.Fn ("=", [tm1,tm2])) =
   1.540 +            list_comb(Const ("op =", HOLogic.typeT), map cvt [tm1,tm2])
   1.541 +        | cvt (t as Metis.Term.Fn (x, [])) =
   1.542 +           (case Recon.strip_prefix ResClause.const_prefix x of
   1.543 +                SOME c => Const (Recon.invert_const c, dummyT)
   1.544 +              | NONE => (*Not a constant. Is it a fixed variable??*)
   1.545 +            case Recon.strip_prefix ResClause.fixed_var_prefix x of
   1.546 +                SOME v => Free (v, dummyT)
   1.547 +              | NONE =>  (trace_msg (fn () => "fol_term_to_hol_FT bad const: " ^ x); fol_term_to_hol_RAW ctxt t))
   1.548 +        | cvt t = (trace_msg (fn () => "fol_term_to_hol_FT bad term: " ^ Metis.Term.toString t); fol_term_to_hol_RAW ctxt t)
   1.549 +  in  cvt fol_tm   end;
   1.550  
   1.551 -  fun fol_term_to_hol ctxt FO = fol_term_to_hol_RAW ctxt
   1.552 -    | fol_term_to_hol ctxt HO = fol_term_to_hol_RAW ctxt
   1.553 -    | fol_term_to_hol ctxt FT = fol_term_to_hol_FT ctxt;
   1.554 +fun fol_term_to_hol ctxt FO = fol_term_to_hol_RAW ctxt
   1.555 +  | fol_term_to_hol ctxt HO = fol_term_to_hol_RAW ctxt
   1.556 +  | fol_term_to_hol ctxt FT = fol_term_to_hol_FT ctxt;
   1.557  
   1.558 -  fun fol_terms_to_hol ctxt mode fol_tms =
   1.559 -    let val ts = map (fol_term_to_hol ctxt mode) fol_tms
   1.560 -        val _ = trace_msg (fn () => "  calling type inference:")
   1.561 -        val _ = app (fn t => trace_msg (fn () => Syntax.string_of_term ctxt t)) ts
   1.562 -        val ts' = infer_types ctxt ts;
   1.563 -        val _ = app (fn t => trace_msg
   1.564 -                      (fn () => "  final term: " ^ Syntax.string_of_term ctxt t ^
   1.565 -                                "  of type  " ^ Syntax.string_of_typ ctxt (type_of t)))
   1.566 -                    ts'
   1.567 -    in  ts'  end;
   1.568 +fun fol_terms_to_hol ctxt mode fol_tms =
   1.569 +  let val ts = map (fol_term_to_hol ctxt mode) fol_tms
   1.570 +      val _ = trace_msg (fn () => "  calling type inference:")
   1.571 +      val _ = app (fn t => trace_msg (fn () => Syntax.string_of_term ctxt t)) ts
   1.572 +      val ts' = infer_types ctxt ts;
   1.573 +      val _ = app (fn t => trace_msg
   1.574 +                    (fn () => "  final term: " ^ Syntax.string_of_term ctxt t ^
   1.575 +                              "  of type  " ^ Syntax.string_of_typ ctxt (type_of t)))
   1.576 +                  ts'
   1.577 +  in  ts'  end;
   1.578  
   1.579 -  fun mk_not (Const ("Not", _) $ b) = b
   1.580 -    | mk_not b = HOLogic.mk_not b;
   1.581 +fun mk_not (Const ("Not", _) $ b) = b
   1.582 +  | mk_not b = HOLogic.mk_not b;
   1.583  
   1.584 -  val metis_eq = Metis.Term.Fn ("=", []);
   1.585 +val metis_eq = Metis.Term.Fn ("=", []);
   1.586  
   1.587 -  (* ------------------------------------------------------------------------- *)
   1.588 -  (* FOL step Inference Rules                                                  *)
   1.589 -  (* ------------------------------------------------------------------------- *)
   1.590 +(* ------------------------------------------------------------------------- *)
   1.591 +(* FOL step Inference Rules                                                  *)
   1.592 +(* ------------------------------------------------------------------------- *)
   1.593  
   1.594 -  (*for debugging only*)
   1.595 -  fun print_thpair (fth,th) =
   1.596 -    (trace_msg (fn () => "=============================================");
   1.597 -     trace_msg (fn () => "Metis: " ^ Metis.Thm.toString fth);
   1.598 -     trace_msg (fn () => "Isabelle: " ^ Display.string_of_thm_without_context th));
   1.599 +(*for debugging only*)
   1.600 +fun print_thpair (fth,th) =
   1.601 +  (trace_msg (fn () => "=============================================");
   1.602 +   trace_msg (fn () => "Metis: " ^ Metis.Thm.toString fth);
   1.603 +   trace_msg (fn () => "Isabelle: " ^ Display.string_of_thm_without_context th));
   1.604  
   1.605 -  fun lookth thpairs (fth : Metis.Thm.thm) =
   1.606 -    valOf (AList.lookup (uncurry Metis.Thm.equal) thpairs fth)
   1.607 -    handle Option => error ("Failed to find a Metis theorem " ^ Metis.Thm.toString fth);
   1.608 +fun lookth thpairs (fth : Metis.Thm.thm) =
   1.609 +  valOf (AList.lookup (uncurry Metis.Thm.equal) thpairs fth)
   1.610 +  handle Option => error ("Failed to find a Metis theorem " ^ Metis.Thm.toString fth);
   1.611  
   1.612 -  fun is_TrueI th = Thm.eq_thm(TrueI,th);
   1.613 +fun is_TrueI th = Thm.eq_thm(TrueI,th);
   1.614  
   1.615 -  fun cterm_incr_types thy idx = cterm_of thy o (map_types (Logic.incr_tvar idx));
   1.616 +fun cterm_incr_types thy idx = cterm_of thy o (map_types (Logic.incr_tvar idx));
   1.617  
   1.618 -  fun inst_excluded_middle thy i_atm =
   1.619 -    let val th = EXCLUDED_MIDDLE
   1.620 -        val [vx] = Term.add_vars (prop_of th) []
   1.621 -        val substs = [(cterm_of thy (Var vx), cterm_of thy i_atm)]
   1.622 -    in  cterm_instantiate substs th  end;
   1.623 +fun inst_excluded_middle thy i_atm =
   1.624 +  let val th = EXCLUDED_MIDDLE
   1.625 +      val [vx] = Term.add_vars (prop_of th) []
   1.626 +      val substs = [(cterm_of thy (Var vx), cterm_of thy i_atm)]
   1.627 +  in  cterm_instantiate substs th  end;
   1.628  
   1.629 -  (* INFERENCE RULE: AXIOM *)
   1.630 -  fun axiom_inf ctxt thpairs th = incr_indexes 1 (lookth thpairs th);
   1.631 -      (*This causes variables to have an index of 1 by default. SEE ALSO mk_var above.*)
   1.632 +(* INFERENCE RULE: AXIOM *)
   1.633 +fun axiom_inf ctxt thpairs th = incr_indexes 1 (lookth thpairs th);
   1.634 +    (*This causes variables to have an index of 1 by default. SEE ALSO mk_var above.*)
   1.635  
   1.636 -  (* INFERENCE RULE: ASSUME *)
   1.637 -  fun assume_inf ctxt mode atm =
   1.638 -    inst_excluded_middle
   1.639 -      (ProofContext.theory_of ctxt)
   1.640 -      (singleton (fol_terms_to_hol ctxt mode) (Metis.Term.Fn atm));
   1.641 +(* INFERENCE RULE: ASSUME *)
   1.642 +fun assume_inf ctxt mode atm =
   1.643 +  inst_excluded_middle
   1.644 +    (ProofContext.theory_of ctxt)
   1.645 +    (singleton (fol_terms_to_hol ctxt mode) (Metis.Term.Fn atm));
   1.646  
   1.647 -  (* INFERENCE RULE: INSTANTIATE (Subst). Type instantiations are ignored. Trying to reconstruct
   1.648 -     them admits new possibilities of errors, e.g. concerning sorts. Instead we try to arrange
   1.649 -     that new TVars are distinct and that types can be inferred from terms.*)
   1.650 -  fun inst_inf ctxt mode thpairs fsubst th =    
   1.651 -    let val thy = ProofContext.theory_of ctxt
   1.652 -        val i_th   = lookth thpairs th
   1.653 -        val i_th_vars = Term.add_vars (prop_of i_th) []
   1.654 -        fun find_var x = valOf (List.find (fn ((a,_),_) => a=x) i_th_vars)
   1.655 -        fun subst_translation (x,y) =
   1.656 -              let val v = find_var x
   1.657 -                  val t = fol_term_to_hol ctxt mode y (*we call infer_types below*)
   1.658 -              in  SOME (cterm_of thy (Var v), t)  end
   1.659 -              handle Option =>
   1.660 -                  (trace_msg (fn() => "List.find failed for the variable " ^ x ^
   1.661 -                                         " in " ^ Display.string_of_thm ctxt i_th);
   1.662 -                   NONE)
   1.663 -        fun remove_typeinst (a, t) =
   1.664 -              case Recon.strip_prefix ResClause.schematic_var_prefix a of
   1.665 -                  SOME b => SOME (b, t)
   1.666 -                | NONE   => case Recon.strip_prefix ResClause.tvar_prefix a of
   1.667 -                  SOME _ => NONE          (*type instantiations are forbidden!*)
   1.668 -                | NONE   => SOME (a,t)    (*internal Metis var?*)
   1.669 -        val _ = trace_msg (fn () => "  isa th: " ^ Display.string_of_thm ctxt i_th)
   1.670 -        val substs = map_filter remove_typeinst (Metis.Subst.toList fsubst)
   1.671 -        val (vars,rawtms) = ListPair.unzip (map_filter subst_translation substs)
   1.672 -        val tms = infer_types ctxt rawtms;
   1.673 -        val ctm_of = cterm_incr_types thy (1 + Thm.maxidx_of i_th)
   1.674 -        val substs' = ListPair.zip (vars, map ctm_of tms)
   1.675 -        val _ = trace_msg (fn () =>
   1.676 -          cat_lines ("subst_translations:" ::
   1.677 -            (substs' |> map (fn (x, y) =>
   1.678 -              Syntax.string_of_term ctxt (term_of x) ^ " |-> " ^
   1.679 -              Syntax.string_of_term ctxt (term_of y)))));
   1.680 -    in  cterm_instantiate substs' i_th  
   1.681 -        handle THM (msg, _, _) => error ("metis error (inst_inf): " ^ msg)
   1.682 -    end;
   1.683 +(* INFERENCE RULE: INSTANTIATE (Subst). Type instantiations are ignored. Trying to reconstruct
   1.684 +   them admits new possibilities of errors, e.g. concerning sorts. Instead we try to arrange
   1.685 +   that new TVars are distinct and that types can be inferred from terms.*)
   1.686 +fun inst_inf ctxt mode thpairs fsubst th =
   1.687 +  let val thy = ProofContext.theory_of ctxt
   1.688 +      val i_th   = lookth thpairs th
   1.689 +      val i_th_vars = Term.add_vars (prop_of i_th) []
   1.690 +      fun find_var x = valOf (List.find (fn ((a,_),_) => a=x) i_th_vars)
   1.691 +      fun subst_translation (x,y) =
   1.692 +            let val v = find_var x
   1.693 +                val t = fol_term_to_hol ctxt mode y (*we call infer_types below*)
   1.694 +            in  SOME (cterm_of thy (Var v), t)  end
   1.695 +            handle Option =>
   1.696 +                (trace_msg (fn() => "List.find failed for the variable " ^ x ^
   1.697 +                                       " in " ^ Display.string_of_thm ctxt i_th);
   1.698 +                 NONE)
   1.699 +      fun remove_typeinst (a, t) =
   1.700 +            case Recon.strip_prefix ResClause.schematic_var_prefix a of
   1.701 +                SOME b => SOME (b, t)
   1.702 +              | NONE   => case Recon.strip_prefix ResClause.tvar_prefix a of
   1.703 +                SOME _ => NONE          (*type instantiations are forbidden!*)
   1.704 +              | NONE   => SOME (a,t)    (*internal Metis var?*)
   1.705 +      val _ = trace_msg (fn () => "  isa th: " ^ Display.string_of_thm ctxt i_th)
   1.706 +      val substs = map_filter remove_typeinst (Metis.Subst.toList fsubst)
   1.707 +      val (vars,rawtms) = ListPair.unzip (map_filter subst_translation substs)
   1.708 +      val tms = infer_types ctxt rawtms;
   1.709 +      val ctm_of = cterm_incr_types thy (1 + Thm.maxidx_of i_th)
   1.710 +      val substs' = ListPair.zip (vars, map ctm_of tms)
   1.711 +      val _ = trace_msg (fn () =>
   1.712 +        cat_lines ("subst_translations:" ::
   1.713 +          (substs' |> map (fn (x, y) =>
   1.714 +            Syntax.string_of_term ctxt (term_of x) ^ " |-> " ^
   1.715 +            Syntax.string_of_term ctxt (term_of y)))));
   1.716 +  in  cterm_instantiate substs' i_th
   1.717 +      handle THM (msg, _, _) => error ("metis error (inst_inf): " ^ msg)
   1.718 +  end;
   1.719  
   1.720 -  (* INFERENCE RULE: RESOLVE *)
   1.721 +(* INFERENCE RULE: RESOLVE *)
   1.722  
   1.723 -  (*Like RSN, but we rename apart only the type variables. Vars here typically have an index
   1.724 -    of 1, and the use of RSN would increase this typically to 3. Instantiations of those Vars
   1.725 -    could then fail. See comment on mk_var.*)
   1.726 -  fun resolve_inc_tyvars(tha,i,thb) =
   1.727 -    let val tha = Drule.incr_type_indexes (1 + Thm.maxidx_of thb) tha
   1.728 -	val ths = Seq.list_of (Thm.bicompose false (false,tha,nprems_of tha) i thb)
   1.729 -    in
   1.730 -	case distinct Thm.eq_thm ths of
   1.731 -	  [th] => th
   1.732 -	| _ => raise THM ("resolve_inc_tyvars: unique result expected", i, [tha,thb])
   1.733 -    end;
   1.734 +(*Like RSN, but we rename apart only the type variables. Vars here typically have an index
   1.735 +  of 1, and the use of RSN would increase this typically to 3. Instantiations of those Vars
   1.736 +  could then fail. See comment on mk_var.*)
   1.737 +fun resolve_inc_tyvars(tha,i,thb) =
   1.738 +  let val tha = Drule.incr_type_indexes (1 + Thm.maxidx_of thb) tha
   1.739 +      val ths = Seq.list_of (Thm.bicompose false (false,tha,nprems_of tha) i thb)
   1.740 +  in
   1.741 +      case distinct Thm.eq_thm ths of
   1.742 +        [th] => th
   1.743 +      | _ => raise THM ("resolve_inc_tyvars: unique result expected", i, [tha,thb])
   1.744 +  end;
   1.745  
   1.746 -  fun resolve_inf ctxt mode thpairs atm th1 th2 =
   1.747 -    let
   1.748 -      val thy = ProofContext.theory_of ctxt
   1.749 -      val i_th1 = lookth thpairs th1 and i_th2 = lookth thpairs th2
   1.750 -      val _ = trace_msg (fn () => "  isa th1 (pos): " ^ Display.string_of_thm ctxt i_th1)
   1.751 -      val _ = trace_msg (fn () => "  isa th2 (neg): " ^ Display.string_of_thm ctxt i_th2)
   1.752 -    in
   1.753 -      if is_TrueI i_th1 then i_th2 (*Trivial cases where one operand is type info*)
   1.754 -      else if is_TrueI i_th2 then i_th1
   1.755 -      else
   1.756 -        let
   1.757 -          val i_atm = singleton (fol_terms_to_hol ctxt mode) (Metis.Term.Fn atm)
   1.758 -          val _ = trace_msg (fn () => "  atom: " ^ Syntax.string_of_term ctxt i_atm)
   1.759 -          val prems_th1 = prems_of i_th1
   1.760 -          val prems_th2 = prems_of i_th2
   1.761 -          val index_th1 = get_index (mk_not i_atm) prems_th1
   1.762 -                handle Empty => error "Failed to find literal in th1"
   1.763 -          val _ = trace_msg (fn () => "  index_th1: " ^ Int.toString index_th1)
   1.764 -          val index_th2 = get_index i_atm prems_th2
   1.765 -                handle Empty => error "Failed to find literal in th2"
   1.766 -          val _ = trace_msg (fn () => "  index_th2: " ^ Int.toString index_th2)
   1.767 -      in  resolve_inc_tyvars (Meson.select_literal index_th1 i_th1, index_th2, i_th2)  end
   1.768 -    end;
   1.769 +fun resolve_inf ctxt mode thpairs atm th1 th2 =
   1.770 +  let
   1.771 +    val thy = ProofContext.theory_of ctxt
   1.772 +    val i_th1 = lookth thpairs th1 and i_th2 = lookth thpairs th2
   1.773 +    val _ = trace_msg (fn () => "  isa th1 (pos): " ^ Display.string_of_thm ctxt i_th1)
   1.774 +    val _ = trace_msg (fn () => "  isa th2 (neg): " ^ Display.string_of_thm ctxt i_th2)
   1.775 +  in
   1.776 +    if is_TrueI i_th1 then i_th2 (*Trivial cases where one operand is type info*)
   1.777 +    else if is_TrueI i_th2 then i_th1
   1.778 +    else
   1.779 +      let
   1.780 +        val i_atm = singleton (fol_terms_to_hol ctxt mode) (Metis.Term.Fn atm)
   1.781 +        val _ = trace_msg (fn () => "  atom: " ^ Syntax.string_of_term ctxt i_atm)
   1.782 +        val prems_th1 = prems_of i_th1
   1.783 +        val prems_th2 = prems_of i_th2
   1.784 +        val index_th1 = get_index (mk_not i_atm) prems_th1
   1.785 +              handle Empty => error "Failed to find literal in th1"
   1.786 +        val _ = trace_msg (fn () => "  index_th1: " ^ Int.toString index_th1)
   1.787 +        val index_th2 = get_index i_atm prems_th2
   1.788 +              handle Empty => error "Failed to find literal in th2"
   1.789 +        val _ = trace_msg (fn () => "  index_th2: " ^ Int.toString index_th2)
   1.790 +    in  resolve_inc_tyvars (Meson.select_literal index_th1 i_th1, index_th2, i_th2)  end
   1.791 +  end;
   1.792  
   1.793 -  (* INFERENCE RULE: REFL *)
   1.794 -  val refl_x = cterm_of @{theory} (Var (hd (Term.add_vars (prop_of REFL_THM) [])));
   1.795 -  val refl_idx = 1 + Thm.maxidx_of REFL_THM;
   1.796 +(* INFERENCE RULE: REFL *)
   1.797 +val refl_x = cterm_of @{theory} (Var (hd (Term.add_vars (prop_of REFL_THM) [])));
   1.798 +val refl_idx = 1 + Thm.maxidx_of REFL_THM;
   1.799  
   1.800 -  fun refl_inf ctxt mode t =
   1.801 -    let val thy = ProofContext.theory_of ctxt
   1.802 -        val i_t = singleton (fol_terms_to_hol ctxt mode) t
   1.803 -        val _ = trace_msg (fn () => "  term: " ^ Syntax.string_of_term ctxt i_t)
   1.804 -        val c_t = cterm_incr_types thy refl_idx i_t
   1.805 -    in  cterm_instantiate [(refl_x, c_t)] REFL_THM  end;
   1.806 +fun refl_inf ctxt mode t =
   1.807 +  let val thy = ProofContext.theory_of ctxt
   1.808 +      val i_t = singleton (fol_terms_to_hol ctxt mode) t
   1.809 +      val _ = trace_msg (fn () => "  term: " ^ Syntax.string_of_term ctxt i_t)
   1.810 +      val c_t = cterm_incr_types thy refl_idx i_t
   1.811 +  in  cterm_instantiate [(refl_x, c_t)] REFL_THM  end;
   1.812  
   1.813 -  fun get_ty_arg_size thy (Const("op =",_)) = 0  (*equality has no type arguments*)
   1.814 -    | get_ty_arg_size thy (Const(c,_))      = (Recon.num_typargs thy c handle TYPE _ => 0)
   1.815 -    | get_ty_arg_size thy _      = 0;
   1.816 +fun get_ty_arg_size thy (Const("op =",_)) = 0  (*equality has no type arguments*)
   1.817 +  | get_ty_arg_size thy (Const(c,_))      = (Recon.num_typargs thy c handle TYPE _ => 0)
   1.818 +  | get_ty_arg_size thy _      = 0;
   1.819  
   1.820 -  (* INFERENCE RULE: EQUALITY *)
   1.821 -  fun equality_inf ctxt mode thpairs (pos,atm) fp fr =
   1.822 -    let val thy = ProofContext.theory_of ctxt
   1.823 -        val m_tm = Metis.Term.Fn atm
   1.824 -        val [i_atm,i_tm] = fol_terms_to_hol ctxt mode [m_tm, fr]
   1.825 -        val _ = trace_msg (fn () => "sign of the literal: " ^ Bool.toString pos)
   1.826 -        fun replace_item_list lx 0 (l::ls) = lx::ls
   1.827 -          | replace_item_list lx i (l::ls) = l :: replace_item_list lx (i-1) ls
   1.828 -        fun path_finder_FO tm [] = (tm, Term.Bound 0)
   1.829 -          | path_finder_FO tm (p::ps) =
   1.830 -              let val (tm1,args) = Term.strip_comb tm
   1.831 -                  val adjustment = get_ty_arg_size thy tm1
   1.832 -                  val p' = if adjustment > p then p else p-adjustment
   1.833 -                  val tm_p = List.nth(args,p')
   1.834 -                    handle Subscript => error ("equality_inf: " ^ Int.toString p ^ " adj " ^
   1.835 -                      Int.toString adjustment  ^ " term " ^  Syntax.string_of_term ctxt tm)
   1.836 -                  val _ = trace_msg (fn () => "path_finder: " ^ Int.toString p ^
   1.837 -                                        "  " ^ Syntax.string_of_term ctxt tm_p)
   1.838 -		  val (r,t) = path_finder_FO tm_p ps
   1.839 -              in
   1.840 -                  (r, list_comb (tm1, replace_item_list t p' args)) 
   1.841 -              end
   1.842 -        fun path_finder_HO tm [] = (tm, Term.Bound 0)
   1.843 -          | path_finder_HO (t$u) (0::ps) = (fn(x,y) => (x, y$u)) (path_finder_HO t ps)
   1.844 -          | path_finder_HO (t$u) (p::ps) = (fn(x,y) => (x, t$y)) (path_finder_HO u ps)
   1.845 -        fun path_finder_FT tm [] _ = (tm, Term.Bound 0)
   1.846 -          | path_finder_FT tm (0::ps) (Metis.Term.Fn ("ti", [t1,t2])) = 
   1.847 -              path_finder_FT tm ps t1
   1.848 -          | path_finder_FT (t$u) (0::ps) (Metis.Term.Fn (".", [t1,t2])) = 
   1.849 -              (fn(x,y) => (x, y$u)) (path_finder_FT t ps t1)
   1.850 -          | path_finder_FT (t$u) (1::ps) (Metis.Term.Fn (".", [t1,t2])) = 
   1.851 -              (fn(x,y) => (x, t$y)) (path_finder_FT u ps t2)
   1.852 -          | path_finder_FT tm ps t = error ("equality_inf, path_finder_FT: path = " ^
   1.853 -                                          space_implode " " (map Int.toString ps) ^ 
   1.854 -                                          " isa-term: " ^  Syntax.string_of_term ctxt tm ^
   1.855 -                                          " fol-term: " ^ Metis.Term.toString t)
   1.856 -        fun path_finder FO tm ps _ = path_finder_FO tm ps
   1.857 -          | path_finder HO (tm as Const("op =",_) $ _ $ _) (p::ps) _ =
   1.858 -               (*equality: not curried, as other predicates are*)
   1.859 -               if p=0 then path_finder_HO tm (0::1::ps)  (*select first operand*)
   1.860 -               else path_finder_HO tm (p::ps)        (*1 selects second operand*)
   1.861 -          | path_finder HO tm (p::ps) (Metis.Term.Fn ("{}", [t1])) =
   1.862 -               path_finder_HO tm ps      (*if not equality, ignore head to skip hBOOL*)
   1.863 -          | path_finder FT (tm as Const("op =",_) $ _ $ _) (p::ps) 
   1.864 -                              (Metis.Term.Fn ("=", [t1,t2])) =
   1.865 -               (*equality: not curried, as other predicates are*)
   1.866 -               if p=0 then path_finder_FT tm (0::1::ps) 
   1.867 -                            (Metis.Term.Fn (".", [Metis.Term.Fn (".", [metis_eq,t1]), t2])) 
   1.868 -                            (*select first operand*)
   1.869 -               else path_finder_FT tm (p::ps) 
   1.870 -                     (Metis.Term.Fn (".", [metis_eq,t2])) 
   1.871 -                     (*1 selects second operand*)
   1.872 -          | path_finder FT tm (p::ps) (Metis.Term.Fn ("{}", [t1])) = path_finder_FT tm ps t1     
   1.873 -               (*if not equality, ignore head to skip the hBOOL predicate*)
   1.874 -          | path_finder FT tm ps t = path_finder_FT tm ps t  (*really an error case!*)
   1.875 -        fun path_finder_lit ((nt as Term.Const ("Not", _)) $ tm_a) idx =
   1.876 -              let val (tm, tm_rslt) = path_finder mode tm_a idx m_tm
   1.877 -              in (tm, nt $ tm_rslt) end
   1.878 -          | path_finder_lit tm_a idx = path_finder mode tm_a idx m_tm
   1.879 -        val (tm_subst, body) = path_finder_lit i_atm fp
   1.880 -        val tm_abs = Term.Abs("x", Term.type_of tm_subst, body)
   1.881 -        val _ = trace_msg (fn () => "abstraction: " ^ Syntax.string_of_term ctxt tm_abs)
   1.882 -        val _ = trace_msg (fn () => "i_tm: " ^ Syntax.string_of_term ctxt i_tm)
   1.883 -        val _ = trace_msg (fn () => "located term: " ^ Syntax.string_of_term ctxt tm_subst)
   1.884 -        val imax = maxidx_of_term (i_tm $ tm_abs $ tm_subst)  (*ill typed but gives right max*)
   1.885 -        val subst' = incr_indexes (imax+1) (if pos then subst_em else ssubst_em)
   1.886 -        val _ = trace_msg (fn () => "subst' " ^ Display.string_of_thm ctxt subst')
   1.887 -        val eq_terms = map (pairself (cterm_of thy))
   1.888 -                           (ListPair.zip (OldTerm.term_vars (prop_of subst'), [tm_abs, tm_subst, i_tm]))
   1.889 -    in  cterm_instantiate eq_terms subst'  end;
   1.890 +(* INFERENCE RULE: EQUALITY *)
   1.891 +fun equality_inf ctxt mode thpairs (pos,atm) fp fr =
   1.892 +  let val thy = ProofContext.theory_of ctxt
   1.893 +      val m_tm = Metis.Term.Fn atm
   1.894 +      val [i_atm,i_tm] = fol_terms_to_hol ctxt mode [m_tm, fr]
   1.895 +      val _ = trace_msg (fn () => "sign of the literal: " ^ Bool.toString pos)
   1.896 +      fun replace_item_list lx 0 (l::ls) = lx::ls
   1.897 +        | replace_item_list lx i (l::ls) = l :: replace_item_list lx (i-1) ls
   1.898 +      fun path_finder_FO tm [] = (tm, Term.Bound 0)
   1.899 +        | path_finder_FO tm (p::ps) =
   1.900 +            let val (tm1,args) = Term.strip_comb tm
   1.901 +                val adjustment = get_ty_arg_size thy tm1
   1.902 +                val p' = if adjustment > p then p else p-adjustment
   1.903 +                val tm_p = List.nth(args,p')
   1.904 +                  handle Subscript => error ("equality_inf: " ^ Int.toString p ^ " adj " ^
   1.905 +                    Int.toString adjustment  ^ " term " ^  Syntax.string_of_term ctxt tm)
   1.906 +                val _ = trace_msg (fn () => "path_finder: " ^ Int.toString p ^
   1.907 +                                      "  " ^ Syntax.string_of_term ctxt tm_p)
   1.908 +                val (r,t) = path_finder_FO tm_p ps
   1.909 +            in
   1.910 +                (r, list_comb (tm1, replace_item_list t p' args))
   1.911 +            end
   1.912 +      fun path_finder_HO tm [] = (tm, Term.Bound 0)
   1.913 +        | path_finder_HO (t$u) (0::ps) = (fn(x,y) => (x, y$u)) (path_finder_HO t ps)
   1.914 +        | path_finder_HO (t$u) (p::ps) = (fn(x,y) => (x, t$y)) (path_finder_HO u ps)
   1.915 +      fun path_finder_FT tm [] _ = (tm, Term.Bound 0)
   1.916 +        | path_finder_FT tm (0::ps) (Metis.Term.Fn ("ti", [t1,t2])) =
   1.917 +            path_finder_FT tm ps t1
   1.918 +        | path_finder_FT (t$u) (0::ps) (Metis.Term.Fn (".", [t1,t2])) =
   1.919 +            (fn(x,y) => (x, y$u)) (path_finder_FT t ps t1)
   1.920 +        | path_finder_FT (t$u) (1::ps) (Metis.Term.Fn (".", [t1,t2])) =
   1.921 +            (fn(x,y) => (x, t$y)) (path_finder_FT u ps t2)
   1.922 +        | path_finder_FT tm ps t = error ("equality_inf, path_finder_FT: path = " ^
   1.923 +                                        space_implode " " (map Int.toString ps) ^
   1.924 +                                        " isa-term: " ^  Syntax.string_of_term ctxt tm ^
   1.925 +                                        " fol-term: " ^ Metis.Term.toString t)
   1.926 +      fun path_finder FO tm ps _ = path_finder_FO tm ps
   1.927 +        | path_finder HO (tm as Const("op =",_) $ _ $ _) (p::ps) _ =
   1.928 +             (*equality: not curried, as other predicates are*)
   1.929 +             if p=0 then path_finder_HO tm (0::1::ps)  (*select first operand*)
   1.930 +             else path_finder_HO tm (p::ps)        (*1 selects second operand*)
   1.931 +        | path_finder HO tm (p::ps) (Metis.Term.Fn ("{}", [t1])) =
   1.932 +             path_finder_HO tm ps      (*if not equality, ignore head to skip hBOOL*)
   1.933 +        | path_finder FT (tm as Const("op =",_) $ _ $ _) (p::ps)
   1.934 +                            (Metis.Term.Fn ("=", [t1,t2])) =
   1.935 +             (*equality: not curried, as other predicates are*)
   1.936 +             if p=0 then path_finder_FT tm (0::1::ps)
   1.937 +                          (Metis.Term.Fn (".", [Metis.Term.Fn (".", [metis_eq,t1]), t2]))
   1.938 +                          (*select first operand*)
   1.939 +             else path_finder_FT tm (p::ps)
   1.940 +                   (Metis.Term.Fn (".", [metis_eq,t2]))
   1.941 +                   (*1 selects second operand*)
   1.942 +        | path_finder FT tm (p::ps) (Metis.Term.Fn ("{}", [t1])) = path_finder_FT tm ps t1
   1.943 +             (*if not equality, ignore head to skip the hBOOL predicate*)
   1.944 +        | path_finder FT tm ps t = path_finder_FT tm ps t  (*really an error case!*)
   1.945 +      fun path_finder_lit ((nt as Term.Const ("Not", _)) $ tm_a) idx =
   1.946 +            let val (tm, tm_rslt) = path_finder mode tm_a idx m_tm
   1.947 +            in (tm, nt $ tm_rslt) end
   1.948 +        | path_finder_lit tm_a idx = path_finder mode tm_a idx m_tm
   1.949 +      val (tm_subst, body) = path_finder_lit i_atm fp
   1.950 +      val tm_abs = Term.Abs("x", Term.type_of tm_subst, body)
   1.951 +      val _ = trace_msg (fn () => "abstraction: " ^ Syntax.string_of_term ctxt tm_abs)
   1.952 +      val _ = trace_msg (fn () => "i_tm: " ^ Syntax.string_of_term ctxt i_tm)
   1.953 +      val _ = trace_msg (fn () => "located term: " ^ Syntax.string_of_term ctxt tm_subst)
   1.954 +      val imax = maxidx_of_term (i_tm $ tm_abs $ tm_subst)  (*ill typed but gives right max*)
   1.955 +      val subst' = incr_indexes (imax+1) (if pos then subst_em else ssubst_em)
   1.956 +      val _ = trace_msg (fn () => "subst' " ^ Display.string_of_thm ctxt subst')
   1.957 +      val eq_terms = map (pairself (cterm_of thy))
   1.958 +                         (ListPair.zip (OldTerm.term_vars (prop_of subst'), [tm_abs, tm_subst, i_tm]))
   1.959 +  in  cterm_instantiate eq_terms subst'  end;
   1.960  
   1.961 -  val factor = Seq.hd o distinct_subgoals_tac;
   1.962 +val factor = Seq.hd o distinct_subgoals_tac;
   1.963  
   1.964 -  fun step ctxt mode thpairs (fol_th, Metis.Proof.Axiom _)                        =
   1.965 -        factor (axiom_inf ctxt thpairs fol_th)
   1.966 -    | step ctxt mode thpairs (_, Metis.Proof.Assume f_atm)                        =
   1.967 -        assume_inf ctxt mode f_atm
   1.968 -    | step ctxt mode thpairs (_, Metis.Proof.Subst(f_subst, f_th1))               =
   1.969 -        factor (inst_inf ctxt mode thpairs f_subst f_th1)
   1.970 -    | step ctxt mode thpairs (_, Metis.Proof.Resolve(f_atm, f_th1, f_th2))        =
   1.971 -        factor (resolve_inf ctxt mode thpairs f_atm f_th1 f_th2)
   1.972 -    | step ctxt mode thpairs (_, Metis.Proof.Refl f_tm)                           =
   1.973 -        refl_inf ctxt mode f_tm
   1.974 -    | step ctxt mode thpairs (_, Metis.Proof.Equality(f_lit, f_p, f_r)) =
   1.975 -        equality_inf ctxt mode thpairs f_lit f_p f_r;
   1.976 +fun step ctxt mode thpairs (fol_th, Metis.Proof.Axiom _)                        =
   1.977 +      factor (axiom_inf ctxt thpairs fol_th)
   1.978 +  | step ctxt mode thpairs (_, Metis.Proof.Assume f_atm)                        =
   1.979 +      assume_inf ctxt mode f_atm
   1.980 +  | step ctxt mode thpairs (_, Metis.Proof.Subst(f_subst, f_th1))               =
   1.981 +      factor (inst_inf ctxt mode thpairs f_subst f_th1)
   1.982 +  | step ctxt mode thpairs (_, Metis.Proof.Resolve(f_atm, f_th1, f_th2))        =
   1.983 +      factor (resolve_inf ctxt mode thpairs f_atm f_th1 f_th2)
   1.984 +  | step ctxt mode thpairs (_, Metis.Proof.Refl f_tm)                           =
   1.985 +      refl_inf ctxt mode f_tm
   1.986 +  | step ctxt mode thpairs (_, Metis.Proof.Equality(f_lit, f_p, f_r)) =
   1.987 +      equality_inf ctxt mode thpairs f_lit f_p f_r;
   1.988  
   1.989 -  fun real_literal (b, (c, _)) = not (String.isPrefix ResClause.class_prefix c);
   1.990 +fun real_literal (b, (c, _)) = not (String.isPrefix ResClause.class_prefix c);
   1.991  
   1.992 -  fun translate mode _    thpairs [] = thpairs
   1.993 -    | translate mode ctxt thpairs ((fol_th, inf) :: infpairs) =
   1.994 -        let val _ = trace_msg (fn () => "=============================================")
   1.995 -            val _ = trace_msg (fn () => "METIS THM: " ^ Metis.Thm.toString fol_th)
   1.996 -            val _ = trace_msg (fn () => "INFERENCE: " ^ Metis.Proof.inferenceToString inf)
   1.997 -            val th = Meson.flexflex_first_order (step ctxt mode thpairs (fol_th, inf))
   1.998 -            val _ = trace_msg (fn () => "ISABELLE THM: " ^ Display.string_of_thm ctxt th)
   1.999 -            val _ = trace_msg (fn () => "=============================================")
  1.1000 -            val n_metis_lits = length (filter real_literal (Metis.LiteralSet.toList (Metis.Thm.clause fol_th)))
  1.1001 -        in
  1.1002 -            if nprems_of th = n_metis_lits then ()
  1.1003 -            else error "Metis: proof reconstruction has gone wrong";
  1.1004 -            translate mode ctxt ((fol_th, th) :: thpairs) infpairs
  1.1005 -        end;
  1.1006 +fun translate mode _    thpairs [] = thpairs
  1.1007 +  | translate mode ctxt thpairs ((fol_th, inf) :: infpairs) =
  1.1008 +      let val _ = trace_msg (fn () => "=============================================")
  1.1009 +          val _ = trace_msg (fn () => "METIS THM: " ^ Metis.Thm.toString fol_th)
  1.1010 +          val _ = trace_msg (fn () => "INFERENCE: " ^ Metis.Proof.inferenceToString inf)
  1.1011 +          val th = Meson.flexflex_first_order (step ctxt mode thpairs (fol_th, inf))
  1.1012 +          val _ = trace_msg (fn () => "ISABELLE THM: " ^ Display.string_of_thm ctxt th)
  1.1013 +          val _ = trace_msg (fn () => "=============================================")
  1.1014 +          val n_metis_lits = length (filter real_literal (Metis.LiteralSet.toList (Metis.Thm.clause fol_th)))
  1.1015 +      in
  1.1016 +          if nprems_of th = n_metis_lits then ()
  1.1017 +          else error "Metis: proof reconstruction has gone wrong";
  1.1018 +          translate mode ctxt ((fol_th, th) :: thpairs) infpairs
  1.1019 +      end;
  1.1020  
  1.1021 -  (*Determining which axiom clauses are actually used*)
  1.1022 -  fun used_axioms axioms (th, Metis.Proof.Axiom _) = SOME (lookth axioms th)
  1.1023 -    | used_axioms axioms _                         = NONE;
  1.1024 +(*Determining which axiom clauses are actually used*)
  1.1025 +fun used_axioms axioms (th, Metis.Proof.Axiom _) = SOME (lookth axioms th)
  1.1026 +  | used_axioms axioms _                         = NONE;
  1.1027  
  1.1028 -  (* ------------------------------------------------------------------------- *)
  1.1029 -  (* Translation of HO Clauses                                                 *)
  1.1030 -  (* ------------------------------------------------------------------------- *)
  1.1031 +(* ------------------------------------------------------------------------- *)
  1.1032 +(* Translation of HO Clauses                                                 *)
  1.1033 +(* ------------------------------------------------------------------------- *)
  1.1034  
  1.1035 -  fun cnf_th thy th = hd (ResAxioms.cnf_axiom thy th);
  1.1036 +fun cnf_th thy th = hd (ResAxioms.cnf_axiom thy th);
  1.1037  
  1.1038 -  val equal_imp_fequal' = cnf_th @{theory} @{thm equal_imp_fequal};
  1.1039 -  val fequal_imp_equal' = cnf_th @{theory} @{thm fequal_imp_equal};
  1.1040 +val equal_imp_fequal' = cnf_th @{theory} @{thm equal_imp_fequal};
  1.1041 +val fequal_imp_equal' = cnf_th @{theory} @{thm fequal_imp_equal};
  1.1042  
  1.1043 -  val comb_I = cnf_th @{theory} ResHolClause.comb_I;
  1.1044 -  val comb_K = cnf_th @{theory} ResHolClause.comb_K;
  1.1045 -  val comb_B = cnf_th @{theory} ResHolClause.comb_B;
  1.1046 -  val comb_C = cnf_th @{theory} ResHolClause.comb_C;
  1.1047 -  val comb_S = cnf_th @{theory} ResHolClause.comb_S;
  1.1048 +val comb_I = cnf_th @{theory} ResHolClause.comb_I;
  1.1049 +val comb_K = cnf_th @{theory} ResHolClause.comb_K;
  1.1050 +val comb_B = cnf_th @{theory} ResHolClause.comb_B;
  1.1051 +val comb_C = cnf_th @{theory} ResHolClause.comb_C;
  1.1052 +val comb_S = cnf_th @{theory} ResHolClause.comb_S;
  1.1053  
  1.1054 -  fun type_ext thy tms =
  1.1055 -    let val subs = ResAtp.tfree_classes_of_terms tms
  1.1056 -        val supers = ResAtp.tvar_classes_of_terms tms
  1.1057 -        and tycons = ResAtp.type_consts_of_terms thy tms
  1.1058 -        val arity_clauses = ResClause.make_arity_clauses thy tycons supers
  1.1059 -        val (supers',arity_clauses) = ResClause.make_arity_clauses thy tycons supers
  1.1060 -        val classrel_clauses = ResClause.make_classrel_clauses thy subs supers'
  1.1061 -    in  map classrel_cls classrel_clauses @ map arity_cls arity_clauses
  1.1062 -    end;
  1.1063 +fun type_ext thy tms =
  1.1064 +  let val subs = ResAtp.tfree_classes_of_terms tms
  1.1065 +      val supers = ResAtp.tvar_classes_of_terms tms
  1.1066 +      and tycons = ResAtp.type_consts_of_terms thy tms
  1.1067 +      val arity_clauses = ResClause.make_arity_clauses thy tycons supers
  1.1068 +      val (supers',arity_clauses) = ResClause.make_arity_clauses thy tycons supers
  1.1069 +      val classrel_clauses = ResClause.make_classrel_clauses thy subs supers'
  1.1070 +  in  map classrel_cls classrel_clauses @ map arity_cls arity_clauses
  1.1071 +  end;
  1.1072  
  1.1073 -  (* ------------------------------------------------------------------------- *)
  1.1074 -  (* Logic maps manage the interface between HOL and first-order logic.        *)
  1.1075 -  (* ------------------------------------------------------------------------- *)
  1.1076 +(* ------------------------------------------------------------------------- *)
  1.1077 +(* Logic maps manage the interface between HOL and first-order logic.        *)
  1.1078 +(* ------------------------------------------------------------------------- *)
  1.1079  
  1.1080 -  type logic_map =
  1.1081 -    {axioms : (Metis.Thm.thm * Thm.thm) list,
  1.1082 -     tfrees : ResClause.type_literal list};
  1.1083 +type logic_map =
  1.1084 +  {axioms : (Metis.Thm.thm * Thm.thm) list,
  1.1085 +   tfrees : ResClause.type_literal list};
  1.1086  
  1.1087 -  fun const_in_metis c (pol,(pred,tm_list)) =
  1.1088 -    let
  1.1089 -      fun in_mterm (Metis.Term.Var nm) = false
  1.1090 -        | in_mterm (Metis.Term.Fn (".", tm_list)) = exists in_mterm tm_list
  1.1091 -        | in_mterm (Metis.Term.Fn (nm, tm_list)) = c=nm orelse exists in_mterm tm_list
  1.1092 -    in  c=pred orelse exists in_mterm tm_list  end;
  1.1093 +fun const_in_metis c (pol,(pred,tm_list)) =
  1.1094 +  let
  1.1095 +    fun in_mterm (Metis.Term.Var nm) = false
  1.1096 +      | in_mterm (Metis.Term.Fn (".", tm_list)) = exists in_mterm tm_list
  1.1097 +      | in_mterm (Metis.Term.Fn (nm, tm_list)) = c=nm orelse exists in_mterm tm_list
  1.1098 +  in  c=pred orelse exists in_mterm tm_list  end;
  1.1099  
  1.1100 -  (*Extract TFree constraints from context to include as conjecture clauses*)
  1.1101 -  fun init_tfrees ctxt =
  1.1102 -    let fun add ((a,i),s) Ts = if i = ~1 then TFree(a,s) :: Ts else Ts
  1.1103 -    in  ResClause.add_typs (Vartab.fold add (#2 (Variable.constraints_of ctxt)) []) end;
  1.1104 +(*Extract TFree constraints from context to include as conjecture clauses*)
  1.1105 +fun init_tfrees ctxt =
  1.1106 +  let fun add ((a,i),s) Ts = if i = ~1 then TFree(a,s) :: Ts else Ts
  1.1107 +  in  ResClause.add_typs (Vartab.fold add (#2 (Variable.constraints_of ctxt)) []) end;
  1.1108  
  1.1109 -  (*transform isabelle type / arity clause to metis clause *)
  1.1110 -  fun add_type_thm [] lmap = lmap
  1.1111 -    | add_type_thm ((ith, mth) :: cls) {axioms, tfrees} =
  1.1112 -        add_type_thm cls {axioms = (mth, ith) :: axioms,
  1.1113 -                          tfrees = tfrees}
  1.1114 +(*transform isabelle type / arity clause to metis clause *)
  1.1115 +fun add_type_thm [] lmap = lmap
  1.1116 +  | add_type_thm ((ith, mth) :: cls) {axioms, tfrees} =
  1.1117 +      add_type_thm cls {axioms = (mth, ith) :: axioms,
  1.1118 +                        tfrees = tfrees}
  1.1119  
  1.1120 -  (*Insert non-logical axioms corresponding to all accumulated TFrees*)
  1.1121 -  fun add_tfrees {axioms, tfrees} : logic_map =
  1.1122 -       {axioms = (map (fn tf => (metis_of_tfree tf, TrueI)) (distinct op= tfrees)) @ axioms,
  1.1123 -        tfrees = tfrees};
  1.1124 +(*Insert non-logical axioms corresponding to all accumulated TFrees*)
  1.1125 +fun add_tfrees {axioms, tfrees} : logic_map =
  1.1126 +     {axioms = (map (fn tf => (metis_of_tfree tf, TrueI)) (distinct op= tfrees)) @ axioms,
  1.1127 +      tfrees = tfrees};
  1.1128  
  1.1129 -  fun string_of_mode FO = "FO"
  1.1130 -    | string_of_mode HO = "HO"
  1.1131 -    | string_of_mode FT = "FT"
  1.1132 +fun string_of_mode FO = "FO"
  1.1133 +  | string_of_mode HO = "HO"
  1.1134 +  | string_of_mode FT = "FT"
  1.1135  
  1.1136 -  (* Function to generate metis clauses, including comb and type clauses *)
  1.1137 -  fun build_map mode0 ctxt cls ths =
  1.1138 -    let val thy = ProofContext.theory_of ctxt
  1.1139 -        (*The modes FO and FT are sticky. HO can be downgraded to FO.*)
  1.1140 -	fun set_mode FO = FO
  1.1141 -	  | set_mode HO = if forall (Meson.is_fol_term thy o prop_of) (cls@ths) then FO else HO
  1.1142 -	  | set_mode FT = FT
  1.1143 -        val mode = set_mode mode0 
  1.1144 -	(*transform isabelle clause to metis clause *)
  1.1145 -	fun add_thm is_conjecture (ith, {axioms, tfrees}) : logic_map =
  1.1146 -	  let val (mth, tfree_lits) = hol_thm_to_fol is_conjecture ctxt mode ith
  1.1147 -	  in
  1.1148 -	     {axioms = (mth, Meson.make_meta_clause ith) :: axioms,
  1.1149 -	      tfrees = tfree_lits union tfrees}
  1.1150 -	  end;
  1.1151 -        val lmap0 = List.foldl (add_thm true)
  1.1152 -                          {axioms = [], tfrees = init_tfrees ctxt} cls
  1.1153 -        val lmap = List.foldl (add_thm false) (add_tfrees lmap0) ths
  1.1154 -        val clause_lists = map (Metis.Thm.clause o #1) (#axioms lmap)
  1.1155 -        fun used c = exists (Metis.LiteralSet.exists (const_in_metis c)) clause_lists
  1.1156 -        (*Now check for the existence of certain combinators*)
  1.1157 -        val thI  = if used "c_COMBI" then [comb_I] else []
  1.1158 -        val thK  = if used "c_COMBK" then [comb_K] else []
  1.1159 -        val thB   = if used "c_COMBB" then [comb_B] else []
  1.1160 -        val thC   = if used "c_COMBC" then [comb_C] else []
  1.1161 -        val thS   = if used "c_COMBS" then [comb_S] else []
  1.1162 -        val thEQ  = if used "c_fequal" then [fequal_imp_equal', equal_imp_fequal'] else []
  1.1163 -        val lmap' = if mode=FO then lmap
  1.1164 -                    else List.foldl (add_thm false) lmap (thEQ @ thS @ thC @ thB @ thK @ thI)
  1.1165 -    in
  1.1166 -        (mode, add_type_thm (type_ext thy (map prop_of (cls @ ths))) lmap')
  1.1167 -    end;
  1.1168 +(* Function to generate metis clauses, including comb and type clauses *)
  1.1169 +fun build_map mode0 ctxt cls ths =
  1.1170 +  let val thy = ProofContext.theory_of ctxt
  1.1171 +      (*The modes FO and FT are sticky. HO can be downgraded to FO.*)
  1.1172 +      fun set_mode FO = FO
  1.1173 +        | set_mode HO = if forall (Meson.is_fol_term thy o prop_of) (cls@ths) then FO else HO
  1.1174 +        | set_mode FT = FT
  1.1175 +      val mode = set_mode mode0
  1.1176 +      (*transform isabelle clause to metis clause *)
  1.1177 +      fun add_thm is_conjecture (ith, {axioms, tfrees}) : logic_map =
  1.1178 +        let val (mth, tfree_lits) = hol_thm_to_fol is_conjecture ctxt mode ith
  1.1179 +        in
  1.1180 +           {axioms = (mth, Meson.make_meta_clause ith) :: axioms,
  1.1181 +            tfrees = tfree_lits union tfrees}
  1.1182 +        end;
  1.1183 +      val lmap0 = List.foldl (add_thm true)
  1.1184 +                        {axioms = [], tfrees = init_tfrees ctxt} cls
  1.1185 +      val lmap = List.foldl (add_thm false) (add_tfrees lmap0) ths
  1.1186 +      val clause_lists = map (Metis.Thm.clause o #1) (#axioms lmap)
  1.1187 +      fun used c = exists (Metis.LiteralSet.exists (const_in_metis c)) clause_lists
  1.1188 +      (*Now check for the existence of certain combinators*)
  1.1189 +      val thI  = if used "c_COMBI" then [comb_I] else []
  1.1190 +      val thK  = if used "c_COMBK" then [comb_K] else []
  1.1191 +      val thB   = if used "c_COMBB" then [comb_B] else []
  1.1192 +      val thC   = if used "c_COMBC" then [comb_C] else []
  1.1193 +      val thS   = if used "c_COMBS" then [comb_S] else []
  1.1194 +      val thEQ  = if used "c_fequal" then [fequal_imp_equal', equal_imp_fequal'] else []
  1.1195 +      val lmap' = if mode=FO then lmap
  1.1196 +                  else List.foldl (add_thm false) lmap (thEQ @ thS @ thC @ thB @ thK @ thI)
  1.1197 +  in
  1.1198 +      (mode, add_type_thm (type_ext thy (map prop_of (cls @ ths))) lmap')
  1.1199 +  end;
  1.1200  
  1.1201 -  fun refute cls =
  1.1202 -      Metis.Resolution.loop (Metis.Resolution.new Metis.Resolution.default cls);
  1.1203 +fun refute cls =
  1.1204 +    Metis.Resolution.loop (Metis.Resolution.new Metis.Resolution.default cls);
  1.1205  
  1.1206 -  fun is_false t = t aconv (HOLogic.mk_Trueprop HOLogic.false_const);
  1.1207 +fun is_false t = t aconv (HOLogic.mk_Trueprop HOLogic.false_const);
  1.1208  
  1.1209 -  fun common_thm ths1 ths2 = exists (member Thm.eq_thm ths1) (map Meson.make_meta_clause ths2);
  1.1210 +fun common_thm ths1 ths2 = exists (member Thm.eq_thm ths1) (map Meson.make_meta_clause ths2);
  1.1211  
  1.1212 -  exception METIS of string;
  1.1213 +exception METIS of string;
  1.1214  
  1.1215 -  (* Main function to start metis prove and reconstruction *)
  1.1216 -  fun FOL_SOLVE mode ctxt cls ths0 =
  1.1217 -    let val thy = ProofContext.theory_of ctxt
  1.1218 -        val th_cls_pairs = map (fn th => (Thm.get_name_hint th, ResAxioms.cnf_axiom thy th)) ths0
  1.1219 -        val ths = maps #2 th_cls_pairs
  1.1220 -        val _ = trace_msg (fn () => "FOL_SOLVE: CONJECTURE CLAUSES")
  1.1221 -        val _ = app (fn th => trace_msg (fn () => Display.string_of_thm ctxt th)) cls
  1.1222 -        val _ = trace_msg (fn () => "THEOREM CLAUSES")
  1.1223 -        val _ = app (fn th => trace_msg (fn () => Display.string_of_thm ctxt th)) ths
  1.1224 -        val (mode, {axioms,tfrees}) = build_map mode ctxt cls ths
  1.1225 -        val _ = if null tfrees then ()
  1.1226 -                else (trace_msg (fn () => "TFREE CLAUSES");
  1.1227 -                      app (fn tf => trace_msg (fn _ => ResClause.tptp_of_typeLit true tf)) tfrees)
  1.1228 -        val _ = trace_msg (fn () => "CLAUSES GIVEN TO METIS")
  1.1229 -        val thms = map #1 axioms
  1.1230 -        val _ = app (fn th => trace_msg (fn () => Metis.Thm.toString th)) thms
  1.1231 -        val _ = trace_msg (fn () => "mode = " ^ string_of_mode mode)
  1.1232 -        val _ = trace_msg (fn () => "START METIS PROVE PROCESS")
  1.1233 -    in
  1.1234 -        case List.filter (is_false o prop_of) cls of
  1.1235 -            false_th::_ => [false_th RS @{thm FalseE}]
  1.1236 -          | [] =>
  1.1237 -        case refute thms of
  1.1238 -            Metis.Resolution.Contradiction mth =>
  1.1239 -              let val _ = trace_msg (fn () => "METIS RECONSTRUCTION START: " ^
  1.1240 -                            Metis.Thm.toString mth)
  1.1241 -                  val ctxt' = fold Variable.declare_constraints (map prop_of cls) ctxt
  1.1242 -                               (*add constraints arising from converting goal to clause form*)
  1.1243 -                  val proof = Metis.Proof.proof mth
  1.1244 -                  val result = translate mode ctxt' axioms proof
  1.1245 -                  and used = map_filter (used_axioms axioms) proof
  1.1246 -                  val _ = trace_msg (fn () => "METIS COMPLETED...clauses actually used:")
  1.1247 -	          val _ = app (fn th => trace_msg (fn () => Display.string_of_thm ctxt th)) used
  1.1248 -	          val unused = filter (fn (a,cls) => not (common_thm used cls)) th_cls_pairs
  1.1249 -              in
  1.1250 -                  if null unused then ()
  1.1251 -                  else warning ("Metis: unused theorems " ^ commas_quote (map #1 unused));
  1.1252 -                  case result of
  1.1253 -                      (_,ith)::_ => 
  1.1254 -                          (trace_msg (fn () => "success: " ^ Display.string_of_thm ctxt ith); 
  1.1255 -                           [ith])
  1.1256 -                    | _ => (trace_msg (fn () => "Metis: no result"); 
  1.1257 -                            [])
  1.1258 -              end
  1.1259 -          | Metis.Resolution.Satisfiable _ => 
  1.1260 -	      (trace_msg (fn () => "Metis: No first-order proof with the lemmas supplied"); 
  1.1261 -	       [])
  1.1262 -    end;
  1.1263 +(* Main function to start metis prove and reconstruction *)
  1.1264 +fun FOL_SOLVE mode ctxt cls ths0 =
  1.1265 +  let val thy = ProofContext.theory_of ctxt
  1.1266 +      val th_cls_pairs = map (fn th => (Thm.get_name_hint th, ResAxioms.cnf_axiom thy th)) ths0
  1.1267 +      val ths = maps #2 th_cls_pairs
  1.1268 +      val _ = trace_msg (fn () => "FOL_SOLVE: CONJECTURE CLAUSES")
  1.1269 +      val _ = app (fn th => trace_msg (fn () => Display.string_of_thm ctxt th)) cls
  1.1270 +      val _ = trace_msg (fn () => "THEOREM CLAUSES")
  1.1271 +      val _ = app (fn th => trace_msg (fn () => Display.string_of_thm ctxt th)) ths
  1.1272 +      val (mode, {axioms,tfrees}) = build_map mode ctxt cls ths
  1.1273 +      val _ = if null tfrees then ()
  1.1274 +              else (trace_msg (fn () => "TFREE CLAUSES");
  1.1275 +                    app (fn tf => trace_msg (fn _ => ResClause.tptp_of_typeLit true tf)) tfrees)
  1.1276 +      val _ = trace_msg (fn () => "CLAUSES GIVEN TO METIS")
  1.1277 +      val thms = map #1 axioms
  1.1278 +      val _ = app (fn th => trace_msg (fn () => Metis.Thm.toString th)) thms
  1.1279 +      val _ = trace_msg (fn () => "mode = " ^ string_of_mode mode)
  1.1280 +      val _ = trace_msg (fn () => "START METIS PROVE PROCESS")
  1.1281 +  in
  1.1282 +      case List.filter (is_false o prop_of) cls of
  1.1283 +          false_th::_ => [false_th RS @{thm FalseE}]
  1.1284 +        | [] =>
  1.1285 +      case refute thms of
  1.1286 +          Metis.Resolution.Contradiction mth =>
  1.1287 +            let val _ = trace_msg (fn () => "METIS RECONSTRUCTION START: " ^
  1.1288 +                          Metis.Thm.toString mth)
  1.1289 +                val ctxt' = fold Variable.declare_constraints (map prop_of cls) ctxt
  1.1290 +                             (*add constraints arising from converting goal to clause form*)
  1.1291 +                val proof = Metis.Proof.proof mth
  1.1292 +                val result = translate mode ctxt' axioms proof
  1.1293 +                and used = map_filter (used_axioms axioms) proof
  1.1294 +                val _ = trace_msg (fn () => "METIS COMPLETED...clauses actually used:")
  1.1295 +                val _ = app (fn th => trace_msg (fn () => Display.string_of_thm ctxt th)) used
  1.1296 +                val unused = filter (fn (a,cls) => not (common_thm used cls)) th_cls_pairs
  1.1297 +            in
  1.1298 +                if null unused then ()
  1.1299 +                else warning ("Metis: unused theorems " ^ commas_quote (map #1 unused));
  1.1300 +                case result of
  1.1301 +                    (_,ith)::_ =>
  1.1302 +                        (trace_msg (fn () => "success: " ^ Display.string_of_thm ctxt ith);
  1.1303 +                         [ith])
  1.1304 +                  | _ => (trace_msg (fn () => "Metis: no result");
  1.1305 +                          [])
  1.1306 +            end
  1.1307 +        | Metis.Resolution.Satisfiable _ =>
  1.1308 +            (trace_msg (fn () => "Metis: No first-order proof with the lemmas supplied");
  1.1309 +             [])
  1.1310 +  end;
  1.1311  
  1.1312 -  fun metis_general_tac mode ctxt ths i st0 =
  1.1313 -    let val _ = trace_msg (fn () =>
  1.1314 -          "Metis called with theorems " ^ cat_lines (map (Display.string_of_thm ctxt) ths))
  1.1315 -    in
  1.1316 -       if exists_type ResAxioms.type_has_empty_sort (prop_of st0)  
  1.1317 -       then (warning "Proof state contains the empty sort"; Seq.empty)
  1.1318 -       else 
  1.1319 -	 (Meson.MESON ResAxioms.neg_clausify
  1.1320 -	   (fn cls => resolve_tac (FOL_SOLVE mode ctxt cls ths) 1) ctxt i
  1.1321 -	  THEN ResAxioms.expand_defs_tac st0) st0
  1.1322 -    end
  1.1323 -    handle METIS s => (warning ("Metis: " ^ s); Seq.empty);
  1.1324 +fun metis_general_tac mode ctxt ths i st0 =
  1.1325 +  let val _ = trace_msg (fn () =>
  1.1326 +        "Metis called with theorems " ^ cat_lines (map (Display.string_of_thm ctxt) ths))
  1.1327 +  in
  1.1328 +     if exists_type ResAxioms.type_has_empty_sort (prop_of st0)
  1.1329 +     then (warning "Proof state contains the empty sort"; Seq.empty)
  1.1330 +     else
  1.1331 +       (Meson.MESON ResAxioms.neg_clausify
  1.1332 +         (fn cls => resolve_tac (FOL_SOLVE mode ctxt cls ths) 1) ctxt i
  1.1333 +        THEN ResAxioms.expand_defs_tac st0) st0
  1.1334 +  end
  1.1335 +  handle METIS s => (warning ("Metis: " ^ s); Seq.empty);
  1.1336  
  1.1337 -  val metis_tac = metis_general_tac HO;
  1.1338 -  val metisF_tac = metis_general_tac FO;
  1.1339 -  val metisFT_tac = metis_general_tac FT;
  1.1340 +val metis_tac = metis_general_tac HO;
  1.1341 +val metisF_tac = metis_general_tac FO;
  1.1342 +val metisFT_tac = metis_general_tac FT;
  1.1343  
  1.1344 -  fun method name mode comment = Method.setup name (Attrib.thms >> (fn ths => fn ctxt =>
  1.1345 -    SIMPLE_METHOD' (CHANGED_PROP o metis_general_tac mode ctxt ths))) comment;
  1.1346 +fun method name mode comment = Method.setup name (Attrib.thms >> (fn ths => fn ctxt =>
  1.1347 +  SIMPLE_METHOD' (CHANGED_PROP o metis_general_tac mode ctxt ths))) comment;
  1.1348  
  1.1349 -  val setup =
  1.1350 -    type_lits_setup #>
  1.1351 -    method @{binding metis} HO "METIS for FOL & HOL problems" #>
  1.1352 -    method @{binding metisF} FO "METIS for FOL problems" #>
  1.1353 -    method @{binding metisFT} FT "METIS With-fully typed translation" #>
  1.1354 -    Method.setup @{binding finish_clausify}
  1.1355 -      (Scan.succeed (K (SIMPLE_METHOD (ResAxioms.expand_defs_tac refl))))
  1.1356 -      "cleanup after conversion to clauses";
  1.1357 +val setup =
  1.1358 +  type_lits_setup #>
  1.1359 +  method @{binding metis} HO "METIS for FOL & HOL problems" #>
  1.1360 +  method @{binding metisF} FO "METIS for FOL problems" #>
  1.1361 +  method @{binding metisFT} FT "METIS With-fully typed translation" #>
  1.1362 +  Method.setup @{binding finish_clausify}
  1.1363 +    (Scan.succeed (K (SIMPLE_METHOD (ResAxioms.expand_defs_tac refl))))
  1.1364 +    "cleanup after conversion to clauses";
  1.1365  
  1.1366  end;