diff options
Diffstat (limited to 'spartan/core/focus.ML')
| -rw-r--r-- | spartan/core/focus.ML | 3 |
1 files changed, 2 insertions, 1 deletions
diff --git a/spartan/core/focus.ML b/spartan/core/focus.ML index 2ad4c8a..b963cfe 100644 --- a/spartan/core/focus.ML +++ b/spartan/core/focus.ML @@ -117,7 +117,8 @@ fun gen_schematic_subgoal prep_atts raw_result_binding param_specs state = |> Proof.map_context (fn _ => #context subgoal_focus |> Proof_Context.note_thmss "" [((Binding.name "prems", []), [(prems, [])])] - |> #2) + |> snd + |> Context_Facts.register_facts prems) |> Proof.internal_goal (K (K ())) (Proof_Context.get_mode ctxt) true "subgoal" NONE after_qed [] [] [(Binding.empty_atts, [(Thm.term_of (#concl subgoal_focus), [])])] |> #2 |