From c06328794736ee370bb8183bcffb4d88a01ea71a Mon Sep 17 00:00:00 2001 From: "Achim D. Brucker" Date: Tue, 29 Aug 2023 06:11:32 +0100 Subject: [PATCH] Isabelle API update. --- Isabelle_DOF/thys/Isa_DOF.thy | 7 ++++--- 1 file changed, 4 insertions(+), 3 deletions(-) diff --git a/Isabelle_DOF/thys/Isa_DOF.thy b/Isabelle_DOF/thys/Isa_DOF.thy index fde5005..f7d615b 100644 --- a/Isabelle_DOF/thys/Isa_DOF.thy +++ b/Isabelle_DOF/thys/Isa_DOF.thy @@ -2562,7 +2562,8 @@ fun gen_theorem schematic bundle_includes prep_att prep_stmt |> prep_statement (prep_att lthy) prep_stmt elems raw_concl; val atts = more_atts @ map (prep_att lthy) raw_atts; - val pos = Position.thread_data (); + val print_cfg = {interactive = int, pos = Position.thread_data (), proof_state= false} + fun after_qed' results goal_ctxt' = let val results' = @@ -2574,12 +2575,12 @@ fun gen_theorem schematic bundle_includes prep_att prep_stmt (map2 (fn (b, _) => fn ths => (b, [(ths, [])])) stmt results') lthy; val lthy'' = if Binding.is_empty_atts (name, atts) then - (Proof_Display.print_results int pos lthy' ((kind, ""), res); lthy') + (Proof_Display.print_results print_cfg lthy' ((kind, ""), res); lthy') else let val ([(res_name, _)], lthy'') = Local_Theory.notes_kind kind [((name, atts), [(maps #2 res, [])])] lthy'; - val _ = Proof_Display.print_results int pos lthy' ((kind, res_name), res); + val _ = Proof_Display.print_results print_cfg lthy' ((kind, res_name), res); in lthy'' end; in after_qed results' lthy'' end;