1.1 --- a/src/Pure/ML/ml_thms.ML	Mon Dec 21 11:55:10 2020 +0100
     1.2 +++ b/src/Pure/ML/ml_thms.ML	Mon Dec 21 15:13:49 2020 +0100
     1.3 @@ -85,11 +85,13 @@
     1.4        (Parse.position by -- Method.parse -- Scan.option Method.parse)))
     1.5      (fn _ => fn ((is_open, raw_propss), (((_, by_pos), m1), m2)) => fn ctxt =>
     1.6        let
     1.7 +        val _ = (**)writeln "##### ML_Thms Theory.setup 1 thm_binding lemma";(**)
     1.8          val reports =
     1.9            (by_pos, Markup.keyword1 |> Markup.keyword_properties) ::
    1.10              maps Method.reports_of (m1 :: the_list m2);
    1.11          val _ = Context_Position.reports ctxt reports;
    1.12  
    1.13 +        val _ = (**)writeln "##### ML_Thms Theory.setup 2 thm_binding lemma";(**)
    1.14          val propss = burrow (map (rpair []) o Syntax.read_props ctxt) raw_propss;
    1.15          val prep_result = Goal.norm_result ctxt #> not is_open ? Thm.close_derivation \<^here>;
    1.16          fun after_qed res goal_ctxt =