# HG changeset patch # User wenzelm # Date 1190908632 -7200 # Node ID cfcdb9817c497703ce46151b693f02a0e025298c # Parent 73b8b42a36b67054f5daa090ecf5ee65964426ec proper handling of chained facts; diff -r 73b8b42a36b6 -r cfcdb9817c49 src/Pure/Tools/invoke.ML --- a/src/Pure/Tools/invoke.ML Thu Sep 27 17:55:28 2007 +0200 +++ b/src/Pure/Tools/invoke.ML Thu Sep 27 17:57:12 2007 +0200 @@ -24,8 +24,9 @@ fun gen_invoke prep_att prep_expr parse_term add_fixes (prfx, raw_atts) raw_expr raw_insts fixes int state = let + val thy = Proof.theory_of state; val _ = Proof.assert_forward_or_chain state; - val thy = Proof.theory_of state; + val chain_facts = if can Proof.assert_chain state then Proof.the_facts state else []; val more_atts = map (prep_att thy) raw_atts; val (elems, _) = prep_expr raw_expr [] (ProofContext.init thy); @@ -39,6 +40,7 @@ val types' = map (Logic.varifyT o TFree) types; val state' = state + |> Proof.enter_forward |> Proof.begin_block |> Proof.map_context (snd o add_fixes fixes); val ctxt' = Proof.context_of state'; @@ -90,6 +92,7 @@ Proof.put_facts NONE #> Seq.single; in state' + |> Proof.chain_facts chain_facts |> Proof.local_goal (K (K ())) (K I) ProofContext.bind_propp_schematic_i "invoke" NONE after_qed propp |> Element.refine_witness