made Sledgehammer's full-typed proof reconstruction work for the first time;
authorblanchet
Fri May 14 11:23:42 2010 +0200 (2010-05-14)
changeset 369097d5587f6d5f7
parent 36908 fb18db78be80
child 36910 dd5a31098f85
made Sledgehammer's full-typed proof reconstruction work for the first time;
previously, Isar proofs and full-type mode were mutually exclusive because both options were hard-coded in the ATP names (e.g., "e_isar" and "full_vampire") -- making the options orthogonal revealed that some code was missing to handle types in the proof reconstruction code
src/HOL/Tools/Sledgehammer/metis_tactics.ML
src/HOL/Tools/Sledgehammer/sledgehammer_fact_minimizer.ML
src/HOL/Tools/Sledgehammer/sledgehammer_hol_clause.ML
src/HOL/Tools/Sledgehammer/sledgehammer_proof_reconstruct.ML
     1.1 --- a/src/HOL/Tools/Sledgehammer/metis_tactics.ML	Fri May 14 11:20:09 2010 +0200
     1.2 +++ b/src/HOL/Tools/Sledgehammer/metis_tactics.ML	Fri May 14 11:23:42 2010 +0200
     1.3 @@ -256,14 +256,13 @@
     1.4              case strip_prefix const_prefix a of
     1.5                  SOME b =>
     1.6                    let val c = invert_const b
     1.7 -                      val ntypes = num_typargs thy c
     1.8 +                      val ntypes = num_type_args thy c
     1.9                        val nterms = length ts - ntypes
    1.10                        val tts = map tm_to_tt ts
    1.11                        val tys = types_of (List.take(tts,ntypes))
    1.12 -                      val ntyargs = num_typargs thy c
    1.13 -                  in if length tys = ntyargs then
    1.14 +                  in if length tys = ntypes then
    1.15                           apply_list (Const (c, dummyT)) nterms (List.drop(tts,ntypes))
    1.16 -                     else error ("Constant " ^ c ^ " expects " ^ Int.toString ntyargs ^
    1.17 +                     else error ("Constant " ^ c ^ " expects " ^ Int.toString ntypes ^
    1.18                                   " but gets " ^ Int.toString (length tys) ^
    1.19                                   " type arguments\n" ^
    1.20                                   cat_lines (map (Syntax.string_of_typ ctxt) tys) ^
    1.21 @@ -460,7 +459,7 @@
    1.22    in  cterm_instantiate [(refl_x, c_t)] REFL_THM  end;
    1.23  
    1.24  fun get_ty_arg_size _ (Const (@{const_name "op ="}, _)) = 0  (*equality has no type arguments*)
    1.25 -  | get_ty_arg_size thy (Const (c, _)) = (num_typargs thy c handle TYPE _ => 0)
    1.26 +  | get_ty_arg_size thy (Const (c, _)) = (num_type_args thy c handle TYPE _ => 0)
    1.27    | get_ty_arg_size _ _ = 0;
    1.28  
    1.29  (* INFERENCE RULE: EQUALITY *)
     2.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_fact_minimizer.ML	Fri May 14 11:20:09 2010 +0200
     2.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_fact_minimizer.ML	Fri May 14 11:23:42 2010 +0200
     2.3 @@ -68,8 +68,8 @@
     2.4  
     2.5  (* minimalization of thms *)
     2.6  
     2.7 -fun minimize_theorems (params as {debug, atps, minimize_timeout, isar_proof,
     2.8 -                                  shrink_factor, ...})
     2.9 +fun minimize_theorems (params as {debug, atps, full_types, minimize_timeout,
    2.10 +                                  isar_proof, shrink_factor, ...})
    2.11                        i n state name_thms_pairs =
    2.12    let
    2.13      val thy = Proof.theory_of state
    2.14 @@ -110,8 +110,8 @@
    2.15          in
    2.16            (SOME min_thms,
    2.17             proof_text isar_proof
    2.18 -                      (pool, debug, shrink_factor, ctxt, conjecture_shape)
    2.19 -                      (K "", proof, internal_thm_names, goal, i) |> fst)
    2.20 +               (pool, debug, full_types, shrink_factor, ctxt, conjecture_shape)
    2.21 +               (K "", proof, internal_thm_names, goal, i) |> fst)
    2.22          end
    2.23      | {outcome = SOME TimedOut, ...} =>
    2.24          (NONE, "Timeout: You can increase the time limit using the \"timeout\" \
     3.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_hol_clause.ML	Fri May 14 11:20:09 2010 +0200
     3.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_hol_clause.ML	Fri May 14 11:23:42 2010 +0200
     3.3 @@ -33,6 +33,7 @@
     3.4    val make_conjecture_clauses : bool -> theory -> thm list -> hol_clause list
     3.5    val make_axiom_clauses : bool -> theory ->
     3.6         (thm * (axiom_name * hol_clause_id)) list -> (axiom_name * hol_clause) list
     3.7 +  val type_wrapper_name : string
     3.8    val get_helper_clauses : bool -> theory -> bool ->
     3.9         hol_clause list * (thm * (axiom_name * hol_clause_id)) list * string list ->
    3.10         hol_clause list
    3.11 @@ -198,8 +199,8 @@
    3.12  (**********************************************************************)
    3.13  
    3.14  (*Result of a function type; no need to check that the argument type matches.*)
    3.15 -fun result_type (TyConstr (("tc_fun", _), [_, tp2])) = tp2
    3.16 -  | result_type _ = raise Fail "Non-function type"
    3.17 +fun result_type (TyConstr (_, [_, tp2])) = tp2
    3.18 +  | result_type _ = raise Fail "non-function type"
    3.19  
    3.20  fun type_of_combterm (CombConst (_, tp, _)) = tp
    3.21    | type_of_combterm (CombVar (_, tp)) = tp
    3.22 @@ -211,7 +212,7 @@
    3.23          |   stripc  x =  x
    3.24      in  stripc(u,[])  end;
    3.25  
    3.26 -val type_wrapper = "ti";
    3.27 +val type_wrapper_name = "ti"
    3.28  
    3.29  fun head_needs_hBOOL explicit_apply const_needs_hBOOL
    3.30                       (CombConst ((c, _), _, _)) =
    3.31 @@ -221,7 +222,7 @@
    3.32  fun wrap_type full_types (s, ty) pool =
    3.33    if full_types then
    3.34      let val (s', pool) = string_of_fol_type ty pool in
    3.35 -      (type_wrapper ^ paren_pack [s, s'], pool)
    3.36 +      (type_wrapper_name ^ paren_pack [s, s'], pool)
    3.37      end
    3.38    else
    3.39      (s, pool)
    3.40 @@ -384,7 +385,7 @@
    3.41  
    3.42  fun decls_of_clauses params clauses arity_clauses =
    3.43    let val functab =
    3.44 -        init_functab |> fold Symtab.update [(type_wrapper, 2), ("hAPP", 2),
    3.45 +        init_functab |> fold Symtab.update [(type_wrapper_name, 2), ("hAPP", 2),
    3.46                                              ("tc_bool", 0)]
    3.47        val predtab = Symtab.empty |> Symtab.update ("hBOOL", 1)
    3.48        val (functab, predtab) =
     4.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_proof_reconstruct.ML	Fri May 14 11:20:09 2010 +0200
     4.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_proof_reconstruct.ML	Fri May 14 11:23:42 2010 +0200
     4.3 @@ -13,7 +13,7 @@
     4.4    val chained_hint: string
     4.5    val invert_const: string -> string
     4.6    val invert_type_const: string -> string
     4.7 -  val num_typargs: theory -> string -> int
     4.8 +  val num_type_args: theory -> string -> int
     4.9    val make_tvar: string -> typ
    4.10    val strip_prefix: string -> string -> string option
    4.11    val metis_line: int -> int -> string list -> string
    4.12 @@ -21,11 +21,11 @@
    4.13      minimize_command * string * string vector * thm * int
    4.14      -> string * string list
    4.15    val isar_proof_text:
    4.16 -    name_pool option * bool * int * Proof.context * int list list
    4.17 +    name_pool option * bool * bool * int * Proof.context * int list list
    4.18      -> minimize_command * string * string vector * thm * int
    4.19      -> string * string list
    4.20    val proof_text:
    4.21 -    bool -> name_pool option * bool * int * Proof.context * int list list
    4.22 +    bool -> name_pool option * bool * bool * int * Proof.context * int list list
    4.23      -> minimize_command * string * string vector * thm * int
    4.24      -> string * string list
    4.25  end;
    4.26 @@ -35,6 +35,7 @@
    4.27  
    4.28  open Sledgehammer_Util
    4.29  open Sledgehammer_FOL_Clause
    4.30 +open Sledgehammer_HOL_Clause
    4.31  open Sledgehammer_Fact_Preprocessor
    4.32  
    4.33  type minimize_command = string list -> string
    4.34 @@ -217,7 +218,7 @@
    4.35  
    4.36  (**** INTERPRETATION OF TSTP SYNTAX TREES ****)
    4.37  
    4.38 -exception NODE of node
    4.39 +exception NODE of node list
    4.40  
    4.41  (*If string s has the prefix s1, return the result of deleting it.*)
    4.42  fun strip_prefix s1 s =
    4.43 @@ -238,16 +239,16 @@
    4.44  fun make_tparam s = TypeInfer.param 0 (s, HOLogic.typeS)
    4.45  fun make_var (b,T) = Var((b,0),T);
    4.46  
    4.47 -(*Type variables are given the basic sort, HOL.type. Some will later be constrained
    4.48 -  by information from type literals, or by type inference.*)
    4.49 -fun type_of_node (u as IntLeaf _) = raise NODE u
    4.50 -  | type_of_node (u as StrNode (a, us)) =
    4.51 -    let val Ts = map type_of_node us in
    4.52 +(* Type variables are given the basic sort "HOL.type". Some will later be
    4.53 +  constrained by information from type literals, or by type inference. *)
    4.54 +fun type_from_node (u as IntLeaf _) = raise NODE [u]
    4.55 +  | type_from_node (u as StrNode (a, us)) =
    4.56 +    let val Ts = map type_from_node us in
    4.57        case strip_prefix tconst_prefix a of
    4.58          SOME b => Type (invert_type_const b, Ts)
    4.59        | NONE =>
    4.60          if not (null us) then
    4.61 -          raise NODE u  (*only tconsts have type arguments*)
    4.62 +          raise NODE [u]  (* only "tconst"s have type arguments *)
    4.63          else case strip_prefix tfree_prefix a of
    4.64            SOME b => TFree ("'" ^ b, HOLogic.typeS)
    4.65          | NONE =>
    4.66 @@ -264,10 +265,8 @@
    4.67  fun invert_const c = c |> Symtab.lookup const_trans_table_inv |> the_default c
    4.68  
    4.69  (*The number of type arguments of a constant, zero if it's monomorphic*)
    4.70 -fun num_typargs thy s = length (Sign.const_typargs thy (s, Sign.the_const_type thy s));
    4.71 -
    4.72 -(*Generates a constant, given its type arguments*)
    4.73 -fun const_of thy (a,Ts) = Const(a, Sign.const_instance thy (a,Ts));
    4.74 +fun num_type_args thy s =
    4.75 +  length (Sign.const_typargs thy (s, Sign.the_const_type thy s))
    4.76  
    4.77  fun fix_atp_variable_name s =
    4.78    let
    4.79 @@ -286,59 +285,81 @@
    4.80      | _ => s
    4.81    end
    4.82  
    4.83 -(*First-order translation. No types are known for variables. HOLogic.typeT should allow
    4.84 -  them to be inferred.*)
    4.85 -fun term_of_node args thy u =
    4.86 -  case u of
    4.87 -    IntLeaf _ => raise NODE u
    4.88 -  | StrNode ("hBOOL", [u]) => term_of_node [] thy u  (* ignore hBOOL *)
    4.89 -  | StrNode ("hAPP", [u1, u2]) => term_of_node (u2 :: args) thy u1
    4.90 -  | StrNode (a, us) =>
    4.91 -    case strip_prefix const_prefix a of
    4.92 -      SOME "equal" =>
    4.93 -      list_comb (Const (@{const_name "op ="}, HOLogic.typeT),
    4.94 -                 map (term_of_node [] thy) us)
    4.95 -    | SOME b =>
    4.96 -      let
    4.97 -        val c = invert_const b
    4.98 -        val nterms = length us - num_typargs thy c
    4.99 -        val ts = map (term_of_node [] thy) (take nterms us @ args)
   4.100 -        (*Extra args from hAPP come AFTER any arguments given directly to the
   4.101 -          constant.*)
   4.102 -        val Ts = map type_of_node (drop nterms us)
   4.103 -      in list_comb(const_of thy (c, Ts), ts) end
   4.104 -    | NONE => (*a variable, not a constant*)
   4.105 -      let
   4.106 -        val opr =
   4.107 -          (* a Free variable is typically a Skolem function *)
   4.108 -          case strip_prefix fixed_var_prefix a of
   4.109 -            SOME b => Free (b, HOLogic.typeT)
   4.110 -          | NONE =>
   4.111 -            case strip_prefix schematic_var_prefix a of
   4.112 -              SOME b => make_var (b, HOLogic.typeT)
   4.113 -            | NONE =>
   4.114 -              (* Variable from the ATP, say "X1" *)
   4.115 -              make_var (fix_atp_variable_name a, HOLogic.typeT)
   4.116 -      in list_comb (opr, map (term_of_node [] thy) (us @ args)) end
   4.117 +(* First-order translation. No types are known for variables. "HOLogic.typeT"
   4.118 +   should allow them to be inferred.*)
   4.119 +fun term_from_node thy full_types =
   4.120 +  let
   4.121 +    fun aux opt_T args u =
   4.122 +      case u of
   4.123 +        IntLeaf _ => raise NODE [u]
   4.124 +      | StrNode ("hBOOL", [u1]) => aux (SOME @{typ bool}) [] u1
   4.125 +      | StrNode ("hAPP", [u1, u2]) => aux opt_T (u2 :: args) u1
   4.126 +      | StrNode ("c_Not", [u1]) => @{const Not} $ aux (SOME @{typ bool}) [] u1
   4.127 +      | StrNode (a, us) =>
   4.128 +        if a = type_wrapper_name then
   4.129 +          case us of
   4.130 +            [term_u, typ_u] => aux (SOME (type_from_node typ_u)) args term_u
   4.131 +          | _ => raise NODE us
   4.132 +        else case strip_prefix const_prefix a of
   4.133 +          SOME "equal" =>
   4.134 +          list_comb (Const (@{const_name "op ="}, HOLogic.typeT),
   4.135 +                     map (aux NONE []) us)
   4.136 +        | SOME b =>
   4.137 +          let
   4.138 +            val c = invert_const b
   4.139 +            val num_type_args = num_type_args thy c
   4.140 +            val actual_num_type_args = if full_types then 0 else num_type_args
   4.141 +            val num_term_args = length us - actual_num_type_args
   4.142 +            val ts = map (aux NONE []) (take num_term_args us @ args)
   4.143 +            val t =
   4.144 +              Const (c, if full_types then
   4.145 +                          case opt_T of
   4.146 +                            SOME T => map fastype_of ts ---> T
   4.147 +                          | NONE =>
   4.148 +                            if num_type_args = 0 then
   4.149 +                              Sign.const_instance thy (c, [])
   4.150 +                            else
   4.151 +                              raise Fail ("no type information for " ^ quote c)
   4.152 +                        else
   4.153 +                          (* Extra args from "hAPP" come after any arguments
   4.154 +                             given directly to the constant. *)
   4.155 +                          Sign.const_instance thy (c,
   4.156 +                                    map type_from_node (drop num_term_args us)))
   4.157 +          in list_comb (t, ts) end
   4.158 +        | NONE => (* a free or schematic variable *)
   4.159 +          let
   4.160 +            val ts = map (aux NONE []) (us @ args)
   4.161 +            val T = map fastype_of ts ---> HOLogic.typeT
   4.162 +            val t =
   4.163 +              case strip_prefix fixed_var_prefix a of
   4.164 +                SOME b => Free (b, T)
   4.165 +              | NONE =>
   4.166 +                case strip_prefix schematic_var_prefix a of
   4.167 +                  SOME b => make_var (b, T)
   4.168 +                | NONE =>
   4.169 +                  (* Variable from the ATP, say "X1" *)
   4.170 +                  make_var (fix_atp_variable_name a, T)
   4.171 +          in list_comb (t, ts) end
   4.172 +  in aux end
   4.173  
   4.174  (* Type class literal applied to a type. Returns triple of polarity, class,
   4.175     type. *)
   4.176 -fun constraint_of_node pos (StrNode ("c_Not", [u])) =
   4.177 -    constraint_of_node (not pos) u
   4.178 -  | constraint_of_node pos u = case u of
   4.179 -        IntLeaf _ => raise NODE u
   4.180 +fun type_constraint_from_node pos (StrNode ("c_Not", [u])) =
   4.181 +    type_constraint_from_node (not pos) u
   4.182 +  | type_constraint_from_node pos u = case u of
   4.183 +        IntLeaf _ => raise NODE [u]
   4.184        | StrNode (a, us) =>
   4.185 -            (case (strip_prefix class_prefix a, map type_of_node us) of
   4.186 +            (case (strip_prefix class_prefix a, map type_from_node us) of
   4.187                   (SOME b, [T]) => (pos, b, T)
   4.188 -               | _ => raise NODE u)
   4.189 +               | _ => raise NODE [u])
   4.190  
   4.191  (** Accumulate type constraints in a clause: negative type literals **)
   4.192  
   4.193  fun add_var (key, z)  = Vartab.map_default (key, []) (cons z)
   4.194  
   4.195 -fun add_constraint ((false, cl, TFree(a,_)), vt) = add_var ((a,~1),cl) vt
   4.196 -  | add_constraint ((false, cl, TVar(ix,_)), vt) = add_var (ix,cl) vt
   4.197 -  | add_constraint (_, vt) = vt;
   4.198 +fun add_type_constraint (false, cl, TFree (a ,_)) = add_var ((a, ~1), cl)
   4.199 +  | add_type_constraint (false, cl, TVar (ix, _)) = add_var (ix, cl)
   4.200 +  | add_type_constraint _ = I
   4.201  
   4.202  fun is_positive_literal (@{const Not} $ _) = false
   4.203    | is_positive_literal t = true
   4.204 @@ -374,10 +395,16 @@
   4.205           |> clause_for_literals thy
   4.206  
   4.207  (*Accumulate sort constraints in vt, with "real" literals in lits.*)
   4.208 -fun lits_of_nodes thy (vt, lits) [] = (vt, finish_clause thy lits)
   4.209 -  | lits_of_nodes thy (vt, lits) (u :: us) =
   4.210 -    lits_of_nodes thy (add_constraint (constraint_of_node true u, vt), lits) us
   4.211 -    handle NODE _ => lits_of_nodes thy (vt, term_of_node [] thy u :: lits) us
   4.212 +fun lits_of_nodes thy full_types (vt, lits) us =
   4.213 +  case us of
   4.214 +    [] => (vt, finish_clause thy lits)
   4.215 +  | (u :: us) =>
   4.216 +    lits_of_nodes thy full_types
   4.217 +        (add_type_constraint (type_constraint_from_node true u) vt, lits) us
   4.218 +    handle NODE _ =>
   4.219 +           lits_of_nodes thy full_types
   4.220 +                         (vt, term_from_node thy full_types (SOME @{typ bool})
   4.221 +                                             [] u :: lits) us
   4.222  
   4.223  (*Update TVars/TFrees with detected sort constraints.*)
   4.224  fun repair_sorts vt =
   4.225 @@ -395,8 +422,9 @@
   4.226    in not (Vartab.is_empty vt) ? do_term end
   4.227  
   4.228  fun unskolemize_term t =
   4.229 -  fold forall_of (Term.add_consts t []
   4.230 -                 |> filter (is_skolem_const_name o fst) |> map Const) t
   4.231 +  Term.add_consts t []
   4.232 +  |> filter (is_skolem_const_name o fst) |> map Const
   4.233 +  |> rpair t |-> fold forall_of
   4.234  
   4.235  val combinator_table =
   4.236    [(@{const_name COMBI}, @{thm COMBI_def_raw}),
   4.237 @@ -416,12 +444,13 @@
   4.238  (* Interpret a list of syntax trees as a clause, given by "real" literals and
   4.239     sort constraints. "vt" holds the initial sort constraints, from the
   4.240     conjecture clauses. *)
   4.241 -fun clause_of_nodes ctxt vt us =
   4.242 -  let val (vt, t) = lits_of_nodes (ProofContext.theory_of ctxt) (vt, []) us in
   4.243 -    t |> repair_sorts vt
   4.244 -  end
   4.245 +fun clause_of_nodes ctxt full_types vt us =
   4.246 +  let
   4.247 +    val thy = ProofContext.theory_of ctxt
   4.248 +    val (vt, t) = lits_of_nodes thy full_types (vt, []) us
   4.249 +  in repair_sorts vt t end
   4.250  fun check_formula ctxt =
   4.251 -  TypeInfer.constrain HOLogic.boolT
   4.252 +  TypeInfer.constrain @{typ bool}
   4.253    #> Syntax.check_term (ProofContext.set_mode ProofContext.mode_schematic ctxt)
   4.254  
   4.255  (** Global sort constraints on TFrees (from tfree_tcs) are positive unit
   4.256 @@ -432,7 +461,7 @@
   4.257  fun tfree_constraints_of_clauses vt [] = vt
   4.258    | tfree_constraints_of_clauses vt ([lit] :: uss) =
   4.259      (tfree_constraints_of_clauses (add_tfree_constraint
   4.260 -                                          (constraint_of_node true lit) vt) uss
   4.261 +                                    (type_constraint_from_node true lit) vt) uss
   4.262       handle NODE _ => (* Not a positive type constraint? Ignore the literal. *)
   4.263       tfree_constraints_of_clauses vt uss)
   4.264    | tfree_constraints_of_clauses vt (_ :: uss) =
   4.265 @@ -447,13 +476,13 @@
   4.266  fun clauses_in_lines (Definition (_, u, us)) = u :: us
   4.267    | clauses_in_lines (Inference (_, us, _)) = us
   4.268  
   4.269 -fun decode_line vt (Definition (num, u, us)) ctxt =
   4.270 +fun decode_line full_types vt (Definition (num, u, us)) ctxt =
   4.271      let
   4.272 -      val t1 = clause_of_nodes ctxt vt [u]
   4.273 +      val t1 = clause_of_nodes ctxt full_types vt [u]
   4.274        val vars = snd (strip_comb t1)
   4.275        val frees = map unvarify_term vars
   4.276        val unvarify_args = subst_atomic (vars ~~ frees)
   4.277 -      val t2 = clause_of_nodes ctxt vt us
   4.278 +      val t2 = clause_of_nodes ctxt full_types vt us
   4.279        val (t1, t2) =
   4.280          HOLogic.eq_const HOLogic.typeT $ t1 $ t2
   4.281          |> unvarify_args |> uncombine_term |> check_formula ctxt
   4.282 @@ -462,19 +491,19 @@
   4.283        (Definition (num, t1, t2),
   4.284         fold Variable.declare_term (maps OldTerm.term_frees [t1, t2]) ctxt)
   4.285      end
   4.286 -  | decode_line vt (Inference (num, us, deps)) ctxt =
   4.287 +  | decode_line full_types vt (Inference (num, us, deps)) ctxt =
   4.288      let
   4.289 -      val t = us |> clause_of_nodes ctxt vt
   4.290 +      val t = us |> clause_of_nodes ctxt full_types vt
   4.291                   |> unskolemize_term |> uncombine_term |> check_formula ctxt
   4.292      in
   4.293        (Inference (num, t, deps),
   4.294         fold Variable.declare_term (OldTerm.term_frees t) ctxt)
   4.295      end
   4.296 -fun decode_lines ctxt lines =
   4.297 +fun decode_lines ctxt full_types lines =
   4.298    let
   4.299      val vt = tfree_constraints_of_clauses Vartab.empty
   4.300                                            (map clauses_in_lines lines)
   4.301 -  in #1 (fold_map (decode_line vt) lines ctxt) end
   4.302 +  in #1 (fold_map (decode_line full_types vt) lines ctxt) end
   4.303  
   4.304  fun aint_inference _ (Definition _) = true
   4.305    | aint_inference t (Inference (_, t', _)) = not (t aconv t')
   4.306 @@ -645,20 +674,20 @@
   4.307            forall_vars t,
   4.308            ByMetis (fold (add_fact_from_dep thm_names) deps ([], [])))
   4.309  
   4.310 -fun proof_from_atp_proof pool ctxt shrink_factor atp_proof conjecture_shape
   4.311 -                         thm_names frees =
   4.312 +fun proof_from_atp_proof pool ctxt full_types shrink_factor atp_proof
   4.313 +                         conjecture_shape thm_names params frees =
   4.314    let
   4.315      val lines =
   4.316        atp_proof ^ "$" (* the $ sign acts as a sentinel *)
   4.317        |> parse_proof pool
   4.318 -      |> decode_lines ctxt
   4.319 +      |> decode_lines ctxt full_types
   4.320        |> rpair [] |-> fold_rev (add_line conjecture_shape thm_names)
   4.321        |> rpair [] |-> fold_rev add_nontrivial_line
   4.322        |> rpair (0, []) |-> fold_rev (add_desired_line ctxt shrink_factor
   4.323                                                 conjecture_shape thm_names frees)
   4.324        |> snd
   4.325    in
   4.326 -    (if null frees then [] else [Fix frees]) @
   4.327 +    (if null params then [] else [Fix params]) @
   4.328      map2 (step_for_line thm_names) (length lines downto 1) lines
   4.329    end
   4.330  
   4.331 @@ -952,17 +981,19 @@
   4.332          do_indent 0 ^ (if n <> 1 then "next" else "qed") ^ "\n"
   4.333    in do_proof end
   4.334  
   4.335 -fun isar_proof_text (pool, debug, shrink_factor, ctxt, conjecture_shape)
   4.336 +fun isar_proof_text (pool, debug, full_types, shrink_factor, ctxt,
   4.337 +                     conjecture_shape)
   4.338                      (minimize_command, atp_proof, thm_names, goal, i) =
   4.339    let
   4.340      val thy = ProofContext.theory_of ctxt
   4.341 -    val (frees, hyp_ts, concl_t) = strip_subgoal goal i
   4.342 +    val (params, hyp_ts, concl_t) = strip_subgoal goal i
   4.343 +    val frees = fold Term.add_frees (concl_t :: hyp_ts) []
   4.344      val n = Logic.count_prems (prop_of goal)
   4.345      val (one_line_proof, lemma_names) =
   4.346        metis_proof_text (minimize_command, atp_proof, thm_names, goal, i)
   4.347      fun isar_proof_for () =
   4.348 -      case proof_from_atp_proof pool ctxt shrink_factor atp_proof
   4.349 -                                conjecture_shape thm_names frees
   4.350 +      case proof_from_atp_proof pool ctxt full_types shrink_factor atp_proof
   4.351 +                                conjecture_shape thm_names params frees
   4.352             |> redirect_proof thy conjecture_shape hyp_ts concl_t
   4.353             |> kill_duplicate_assumptions_in_proof
   4.354             |> then_chain_proof