src/HOL/Tools/res_atp.ML
changeset 25492 4cc7976948ac
parent 25243 78f8aaa27493
child 25761 466e714de2fc
     1.1 --- a/src/HOL/Tools/res_atp.ML	Wed Nov 28 16:16:01 2007 +0100
     1.2 +++ b/src/HOL/Tools/res_atp.ML	Wed Nov 28 16:26:03 2007 +0100
     1.3 @@ -823,8 +823,11 @@
     1.4  
     1.5  fun sledgehammer state =
     1.6    let
     1.7 -    val (ctxt, (chain_ths, goal)) = Proof.get_goal (Toplevel.proof_of state);
     1.8 -    val thy = ProofContext.theory_of ctxt;
     1.9 +    val (ctxt, (chain_ths, goal)) = Proof.get_goal (Toplevel.proof_of state)
    1.10 +    val chain_ths = map (PureThy.put_name_hint Recon.chained_hint) chain_ths
    1.11 +                    (*Mark the chained theorems to keep them out of metis calls;
    1.12 +                      their original "name hints" may be bad anyway.*)
    1.13 +    val thy = ProofContext.theory_of ctxt
    1.14    in
    1.15      Output.debug (fn () => "subgoals in isar_atp:\n" ^
    1.16                    Syntax.string_of_term ctxt (Logic.mk_conjunction_list (Thm.prems_of goal)));