# HG changeset patch # User wenzelm # Date 1606334923 -3600 # Node ID d76b0f29c8fd4f08cb8b0170ad7bac39ef1fcf3e # Parent 9e89c2e15d3626ab612da709a6c980f1870e1fe6 recovered document output from 6bc199a70bf9; diff -r 9e89c2e15d36 -r d76b0f29c8fd src/Pure/Thy/thy_info.ML --- a/src/Pure/Thy/thy_info.ML Wed Nov 25 20:48:33 2020 +0100 +++ b/src/Pure/Thy/thy_info.ML Wed Nov 25 21:08:43 2020 +0100 @@ -56,7 +56,7 @@ ); fun apply_presentation (context: presentation_context) thy = - (ignore (Par_List.map (fn (f, _) => f context thy (Presentation.get thy))); + (ignore (Presentation.get thy |> Par_List.map (fn (f, _) => f context thy)); Output.try_protocol_message (Markup.finished_theory (Context.theory_long_name thy)) []); fun add_presentation f = Presentation.map (cons (f, stamp ()));