1.1 --- a/src/HOL/SPARK/Examples/Gcd/Greatest_Common_Divisor.thy	Mon Dec 21 15:13:49 2020 +0100
     1.2 +++ b/src/HOL/SPARK/Examples/Gcd/Greatest_Common_Divisor.thy	Tue Jan 05 17:29:39 2021 +0100
     1.3 @@ -23,9 +23,9 @@
     1.4    from \<open>0 < d\<close> have "0 \<le> c mod d" by (rule pos_mod_sign)
     1.5  (*^^^^^^^^^^^^-Syntax.read_props..Output.report
     1.6                 ^^^^^^^^^^^^^^^^^-Proof.gen_have..Output.report 2x
     1.7 -                                  ^^^^^^^^^^^^^^^^^^^^^^-have 0 \<le> c mod d*)
     1.8 +                                  ^^^^^^^^^^^^^^^^^^^^^^-"have 0 \<le> c mod d"*)
     1.9    with \<open>0 \<le> c\<close> \<open>0 < d\<close> \<open>c - c sdiv d * d \<noteq> 0\<close> show ?C1
    1.10 -(*^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^-Proof.gen_show....Output.report 2x
    1.11 +(*^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^-Syntax.read_props..Output.report 2x
    1.12                                                 ^^^^^^^^-Proof.gen_show..Output.report 2x*)
    1.13      by (simp add: sdiv_pos_pos minus_div_mult_eq_mod [symmetric])
    1.14  (*  ^^^ Successful attempt to solve goal by exported rule: 0 < c - c sdiv d * d*)
    1.15 @@ -55,7 +55,7 @@
    1.16    but both NOT by ...                                      by (rule pos_mod_sign)
    1.17  # Private_Output.report seems to have "" as argument frequently
    1.18  # Output.report provided semantic annotations in Naproche;
    1.19 -  thus ALL calls of Output.report (in src/Pure) are traced an show up at these elements:
    1.20 +  thus ALL calls of Output.report (in src/Pure) are traced and show up at these elements:
    1.21      proof                                        x  x  .  .  .  
    1.22      from \<open>0 < d\<close>                                 x  .  x  x  x  
    1.23      have "0 \<le> c mod d"                           x  .  x  x  .  
    1.24 @@ -75,8 +75,8 @@
    1.25  \<close>
    1.26  
    1.27  subsection \<open>tracing calls of Output.report\<close>
    1.28 +subsubsection \<open>click on "proof -"\<close>
    1.29  text \<open>
    1.30 -(*--------- click on "proof -" --------
    1.31  ### Private_Output.report keyword1
    1.32  ### Private_Output.report language
    1.33  ### Private_Output.report entityo
    1.34 @@ -85,8 +85,8 @@
    1.35  ### Private_Output.report 
    1.36  ### Token.syntax_generic, Scan.error
    1.37  \<close>
    1.38 +subsubsection \<open>click on "from \<open>0 < d\<close>"\<close>
    1.39  text \<open>
    1.40 -(*--------- click on "from \<open>0 < d\<close>" --------
    1.41  ### Private_Output.report keyword1
    1.42  ### Private_Output.report cartouch
    1.43  ### Private_Output.report delimite
    1.44 @@ -101,14 +101,16 @@
    1.45  ### Context_Position.report_generic           //--- different to subsequent part below
    1.46  ### Private_Output.report entityo
    1.47  \<close>
    1.48 +subsubsection \<open>click on "have "0 \<le> c mod d""\<close>
    1.49  text \<open>
    1.50 -(*--------- click on "have "0 \<le> c mod d"" --------
    1.51 -### Private_Output.report keyword1
    1.52 +### Private_Output.report keyword1                 
    1.53  ### Private_Output.report 
    1.54  ### Private_Output.report cartouch
    1.55  ### Private_Output.report delimite
    1.56  ### Private_Output.report entityo
    1.57  ####-# Proof.gen_have 
    1.58 +###-# Proof_Context.prep_statement 
    1.59 +###-# Proof_Context.prep_stmt
    1.60  ##### Syntax.read_props 
    1.61  #### Syntax_Phases.check_props
    1.62  ### Syntax_Phases.check_terms 
    1.63 @@ -120,14 +122,98 @@
    1.64  #### Syntax_Phases.check_props
    1.65  ### Syntax_Phases.check_terms
    1.66  ### Syntax_Phases.check_typs
    1.67 -## calling Output.report\<close>
    1.68 +## calling Output.report
    1.69 +\<close>
    1.70 +subsubsection \<open>click on "with \<open>0 \<le> c\<close> \<open>0 < d\<close> .."\<close>
    1.71 +text \<open>
    1.72 +##### Syntax.read_props 
    1.73 +#### Syntax_Phases.check_props 
    1.74 +### Syntax_Phases.check_terms 
    1.75 +### Syntax_Phases.check_typs 
    1.76 +### Syntax_Phases.check_typs 
    1.77 +## calling Output.report 
    1.78 +##### Syntax.read_props 
    1.79 +#### Syntax_Phases.check_props 
    1.80 +### Syntax_Phases.check_terms 
    1.81 +### Syntax_Phases.check_typs 
    1.82 +### Syntax_Phases.check_typs 
    1.83 +## calling Output.report 
    1.84 +##### Syntax.read_props 
    1.85 +#### Syntax_Phases.check_props 
    1.86 +### Syntax_Phases.check_terms 
    1.87 +### Syntax_Phases.check_typs 
    1.88 +### Syntax_Phases.check_typs 
    1.89 +## calling Output.report
    1.90 +\<close>
    1.91 +subsubsection \<open>click on "show ?C1"\<close>
    1.92 +text \<open>
    1.93 +###### Proof.gen_show 
    1.94 +##### Syntax.read_props 
    1.95 +#### Syntax_Phases.check_props 
    1.96 +### Syntax_Phases.check_terms 
    1.97 +### Syntax_Phases.check_typs 
    1.98 +### Syntax_Phases.check_typs 
    1.99 +## calling Output.report 
   1.100 +##### Syntax.read_props 
   1.101 +#### Syntax_Phases.check_props 
   1.102 +### Syntax_Phases.check_terms 
   1.103 +### Syntax_Phases.check_typs 
   1.104 +## calling Output.report
   1.105 +\<close>
   1.106 +
   1.107 +subsection \<open>fill gaps in traces \<close>
   1.108 +subsubsection \<open>at beginning of "have "0 \<le> c mod d""\<close>
   1.109 +text \<open>
   1.110 +  WHAT HAS BEEN OBSERVED / DONE
   1.111 +    click on "have "0 \<le> c mod d"" traces ####-# Proof.gen_have.
   1.112 +    "gen_have" occurs only in proof.ML, there is NO "open Proof" in src/Pure
   1.113 +    "gen_have" is ONLY called by Proof.have, Proof.have_cmd
   1.114 +    Proof.have, Proof.have_cmd are not re-used in proof.ML; 
   1.115 +    Proof.have is ONLY called by Obtain.gen_consider, Obtain.gen_obtain
   1.116 +    Obtain.gen_consider, Obtain.gen_obtain DO NOT SHOW UP IN traces ?!?
   1.117 +    TODO
   1.118 +    TODO
   1.119 +  TODO
   1.120 +  TODO
   1.121 +\<close>
   1.122 +
   1.123 +subsubsection \<open>between Proof.gen_have .. Syntax.read_props\<close>
   1.124 +text \<open>
   1.125 +  WHAT HAS BEEN OBSERVED / DONE (search bottom up..)
   1.126 +    Syntax.read_props callers..
   1.127 +      in Syntax.:
   1.128 +        read_prop
   1.129 +          read_prop_global:                     not in trace--//
   1.130 +      in src/Pure (NO "open Syntax")
   1.131 +        Expression.read_full_context_statement  not in trace--//
   1.132 +        Proof_Context.read_propp                not in trace--//
   1.133 +        ML_Thms: val _ = Theory.setup..thm_binding "lemma"..propss:
   1.134 +                                                ?in trace ?!?
   1.135 +          TODO ?!?
   1.136 +          TODO ?!?
   1.137 +          TODO ?!?
   1.138 +    TODO
   1.139 +    TODO ^v^v^v^v^v^v^v^v^--- gap to be closed (by insertion into above)
   1.140 +    TODO
   1.141 +    Proof_Context.prep_statement callers..
   1.142 +      in Proof_Context.:
   1.143 +          cert_statement                        not in trace--//
   1.144 +          read_statement                        not in trace--//
   1.145 +      in src/Pure (NO "open Proof_Context")     ..\<nexists> ----------//
   1.146 +        TODO ?!?
   1.147 +        TODO ?!?
   1.148 +        TODO ?!?
   1.149 +\<close>
   1.150  
   1.151  subsection \<open>signatures of the traced callers of Private_Output.report\<close>
   1.152 -declare [[ML_print_depth = 99999]]
   1.153 +(** )declare [[ML_print_depth = 99999]]( **)
   1.154  ML \<open>
   1.155  \<close> ML \<open>
   1.156 -Token.syntax_generic           : 'a Token.context_parser -> Token.src -> Context.generic ->
   1.157 -                                   'a * Context.generic;
   1.158 +(*'a \<rightarrow> term,                             *)
   1.159 +Token.syntax_generic           : 'a Token.context_parser ->
   1.160 +                                   Token.src -> Context.generic -> 'a * Context.generic;
   1.161 +Token.syntax_generic           : (Context.generic * Token.T list -> 'a * (Context.generic * Token.T list)) ->
   1.162 +                                   Token.src -> Context.generic -> 'a * Context.generic;
   1.163  Context_Position.report_generic: Context.generic -> Position.T -> Markup.T -> unit;
   1.164  Private_Output.report          : string(*= markup*) list                   -> unit; 
   1.165  (*Syntax_Phases.check_typs     : Proof.context -> typ list -> typ list;    ..local*)
   1.166 @@ -159,7 +245,8 @@
   1.167  \<close> ML \<open>
   1.168  \<close>
   1.169  
   1.170 -subsection \<open>lookup calls of Syntax_Phases.check_terms\<close>
   1.171 +subsection \<open>lookup ALL calls of ..\<close>
   1.172 +subsubsection \<open>of Syntax_Phases.check_terms\<close>
   1.173  text \<open>
   1.174    focus are    "from \<open>0 < d\<close>"   and   have "0 \<le> c mod d".
   1.175  
   1.176 @@ -185,7 +272,7 @@
   1.177      
   1.178  \<close>
   1.179  
   1.180 -subsection \<open>lookup calls of Syntax.read_props\<close>
   1.181 +subsubsection \<open>of Syntax.read_props\<close>
   1.182  text \<open>
   1.183    focus are    "from \<open>0 < d\<close>"   and   have "0 \<le> c mod d".
   1.184    NO open Syntax_Phases, Syntax in src/Pure
   1.185 @@ -197,34 +284,15 @@
   1.186      Proof_Context.read_propp
   1.187      Expression.read_full_context_statement
   1.188      
   1.189 -    ??? where else might Syntax.read_props be called ???
   1.190 +    ??? where else might Syntax.read_props be called: found ####-# Proof.gen_have
   1.191      
   1.192    search top down
   1.193 -    "from" :: prf_chain % "proof"        only def.in Pure.thy: "from" "with"
   1.194 +    "from" :: prf_chain % "proof"        only def.in Pure.thy, \<notin> src/Pure
   1.195 +    "with" :: prf_chain % "proof"        only def.in Pure.thy, \<in> src/Pure in ml_lex.ML/scala
   1.196      "have" :: prf_goal % "proof"         -"- + Proof.have
   1.197      "show" :: prf_asm_goal % "proof"     -"- + Proof.show
   1.198  \<close>
   1.199  
   1.200 -subsection \<open>TODO: fill gap Syntax.read_props .. Proof.gen_have\<close>
   1.201 -text \<open>
   1.202 -  TODO: fill the gap in the trace between Syntax.read_props .. Proof.gen_have.
   1.203 -\<close>
   1.204 -
   1.205 -subsection \<open>lookup calls of Proof.have.."have"\<close>
   1.206 -text \<open>
   1.207 -  Proof.have
   1.208 -  Proof.have_cmd
   1.209 -  Proof.show
   1.210 -  Proof.show_cmd
   1.211 -  Obtain.gen_consider
   1.212 -  Obtain.gen_obtain
   1.213 -    
   1.214 -    ??? where else might Proof.have (current hd of trace) be called ???
   1.215 -    NO "open Proof" in src/Pure
   1.216 -    !!! there are new trace elements Proof.* (found in other parts of spark_vc procedure_g_c_d_4)
   1.217 -    
   1.218 -\<close>
   1.219 -
   1.220  subsubsection \<open>TODO\<close>
   1.221  text \<open>
   1.222    TODO

     2.1 --- a/src/Pure/Isar/expression.ML	Mon Dec 21 15:13:49 2020 +0100
     2.2 +++ b/src/Pure/Isar/expression.ML	Tue Jan 05 17:29:39 2021 +0100
     2.3 @@ -501,6 +501,9 @@
     2.4  
     2.5  fun cert_statement x = prep_statement cert_full_context_statement Element.activate_i x;
     2.6  fun read_statement x = prep_statement read_full_context_statement Element.activate x;
     2.7 +fun read_statement x =
     2.8 +  ((**)writeln "###-# Expression.read_statement";(**)
     2.9 +    prep_statement read_full_context_statement Element.activate x);
    2.10  
    2.11  (*5*)end;(*5*)
    2.12  
    2.13 @@ -533,6 +536,9 @@
    2.14  fun cert_declaration x = prep_declaration cert_full_context_statement Element.activate_i x;
    2.15  fun cert_read_declaration x = prep_declaration cert_read_full_context_statement Element.activate x;
    2.16  fun read_declaration x = prep_declaration read_full_context_statement Element.activate x;
    2.17 +fun read_declaration x =
    2.18 +((**)writeln "##### Expression.read_declaration";(**)
    2.19 +    prep_declaration read_full_context_statement Element.activate x);
    2.20  
    2.21  (*6*)end;(*6*)
    2.22  
    2.23 @@ -547,6 +553,7 @@
    2.24  
    2.25  fun prep_goal_expression prep expression ctxt =
    2.26    let
    2.27 +    val _ = writeln "###-# Expression.prep_goal_expression";
    2.28      val thy = Proof_Context.theory_of ctxt;
    2.29  
    2.30      val ((fixed, deps, eqnss, _, _), _) =
    2.31 @@ -573,6 +580,9 @@
    2.32  
    2.33  fun cert_goal_expression x = prep_goal_expression cert_full_context_statement x;
    2.34  fun read_goal_expression x = prep_goal_expression read_full_context_statement x;
    2.35 +fun read_goal_expression x =
    2.36 +  ((**)writeln "##### Expression.read_goal_expression";(**)
    2.37 +    prep_goal_expression read_full_context_statement x);
    2.38  
    2.39  (*7*)end;(*7*)
    2.40  

     3.1 --- a/src/Pure/Isar/interpretation.ML	Mon Dec 21 15:13:49 2020 +0100
     3.2 +++ b/src/Pure/Isar/interpretation.ML	Tue Jan 05 17:29:39 2021 +0100
     3.3 @@ -67,6 +67,7 @@
     3.4  fun prep_interpretation prep_expr prep_term
     3.5    expression raw_defs initial_ctxt =
     3.6    let
     3.7 +    val _ = writeln "###-# Interpretation.prep_interpretation";
     3.8      val ((propss, eq_propss, deps, eqnss, export), expr_ctxt) = prep_expr expression initial_ctxt;
     3.9      val (def_eqns, def_ctxt) =
    3.10        augment_with_defs prep_term raw_defs deps expr_ctxt;
    3.11 @@ -118,6 +119,7 @@
    3.12  fun generic_interpretation prep_interpretation setup_proof note add_registration
    3.13      expression raw_defs initial_ctxt =
    3.14    let
    3.15 +    val _ = writeln "###-# Interpretation.generic_interpretation";
    3.16      val (((propss, eq_propss, deps, eqnss, export, export'), def_eqns), goal_ctxt) =
    3.17        prep_interpretation expression raw_defs initial_ctxt;
    3.18      fun after_qed witss eqns =
    3.19 @@ -147,7 +149,14 @@
    3.20  in
    3.21  
    3.22  val interpret = gen_interpret cert_interpretation;
    3.23 +val interpret =
    3.24 +  (writeln "###-# Interpretation.interpret";
    3.25 +    gen_interpret cert_interpretation);
    3.26 +
    3.27  val interpret_cmd = gen_interpret read_interpretation;
    3.28 +val interpret_cmd =
    3.29 +  (writeln "###-# Interpretation.interpret_cmd";
    3.30 +    gen_interpret read_interpretation);
    3.31  
    3.32  end;
    3.33  

     4.1 --- a/src/Pure/Isar/proof.ML	Mon Dec 21 15:13:49 2020 +0100
     4.2 +++ b/src/Pure/Isar/proof.ML	Tue Jan 05 17:29:39 2021 +0100
     4.3 @@ -720,14 +720,29 @@
     4.4  val note_thmss_cmd = gen_thmss (K []) I #2 Attrib.attribute_cmd Proof_Context.get_fact;
     4.5  
     4.6  val from_thmss = gen_thmss (K []) chain #2 (K I) (K I) o empty_bindings;
     4.7 +val from_thmss =
     4.8 +  ((**)writeln "####-# Proof.from_thmss";(**)
     4.9 +    gen_thmss (K []) chain #2 (K I) (K I) o empty_bindings);
    4.10  val from_thmss_cmd =
    4.11    gen_thmss (K []) chain #2 Attrib.attribute_cmd Proof_Context.get_fact o empty_bindings;
    4.12 +val from_thmss_cmd =
    4.13 +  ((**)writeln "####-# Proof.from_thmss_cmd";(**)
    4.14 +    gen_thmss (K []) chain #2 Attrib.attribute_cmd Proof_Context.get_fact o empty_bindings);
    4.15  
    4.16  val with_thmss = gen_thmss the_facts chain #2 (K I) (K I) o empty_bindings;
    4.17 +val with_thmss =
    4.18 +  ((**)writeln "####-# Proof.with_thmss";(**)
    4.19 +    gen_thmss the_facts chain #2 (K I) (K I) o empty_bindings);
    4.20  val with_thmss_cmd =
    4.21    gen_thmss the_facts chain #2 Attrib.attribute_cmd Proof_Context.get_fact o empty_bindings;
    4.22 +val with_thmss_cmd =
    4.23 +  ((**)writeln "####-# Proof.with_thmss_cmd";(**)
    4.24 +    gen_thmss the_facts chain #2 Attrib.attribute_cmd Proof_Context.get_fact o empty_bindings);
    4.25  
    4.26  val local_results = gen_thmss (K []) I I (K I) (K I) o map (apsnd Thm.simple_fact);
    4.27 +val local_results =
    4.28 +  (writeln "####-# Proof.local_results";
    4.29 +    gen_thmss (K []) I I (K I) (K I) o map (apsnd Thm.simple_fact));
    4.30  
    4.31  (*8*)end;(*8*)
    4.32  
    4.33 @@ -817,6 +832,7 @@
    4.34  
    4.35  fun gen_define prep_stmt prep_att raw_decls raw_fixes raw_defs state =
    4.36    let
    4.37 +    val _ = writeln "###-# Proof.gen_define";
    4.38      val _ = assert_forward state;
    4.39      val ctxt = context_of state;
    4.40  

     5.1 --- a/src/Pure/Isar/proof_context.ML	Mon Dec 21 15:13:49 2020 +0100
     5.2 +++ b/src/Pure/Isar/proof_context.ML	Tue Jan 05 17:29:39 2021 +0100
     5.3 @@ -904,7 +904,9 @@
     5.4  in
     5.5  
     5.6  val cert_propp = prep_propp (map o cert_prop);
     5.7 -val read_propp = ((**)writeln "##### Proof_Context.read_propp";(**) prep_propp Syntax.read_props);
     5.8 +val read_propp =
     5.9 +  ((**)writeln "##### Proof_Context.read_propp";(**)
    5.10 +    prep_propp Syntax.read_props);
    5.11  
    5.12  end;
    5.13  
    5.14 @@ -1251,6 +1253,7 @@
    5.15  
    5.16  fun gen_assms prep_propp exp args ctxt =
    5.17    let
    5.18 +    val _ = writeln "###-# Proof_Context.gen_assms";
    5.19      val (propss, binds) = prep_propp ctxt (map snd args);
    5.20      val props = flat propss;
    5.21    in
    5.22 @@ -1378,11 +1381,12 @@
    5.23  
    5.24  fun prep_stmt prep_var prep_propp raw_vars raw_propps ctxt =
    5.25    let
    5.26 +(**)val _ = writeln "###-# Proof_Context.prep_stmt";(**)
    5.27      val (vars, vars_ctxt) = fold_map prep_var raw_vars ctxt;
    5.28      val xs = map (Variable.check_name o #1) vars;
    5.29      val (xs', fixes_ctxt) = add_fixes vars vars_ctxt;
    5.30  
    5.31 -    val (propss, binds) = prep_propp fixes_ctxt raw_propps;
    5.32 +    val (propss, binds) = prep_propp fixes_ctxt raw_propps;(*<--*)
    5.33      val (ps, params_ctxt) = fixes_ctxt
    5.34        |> (fold o fold) Variable.declare_term propss
    5.35        |> fold_map inferred_param xs';
    5.36 @@ -1401,8 +1405,9 @@
    5.37  
    5.38  fun prep_statement prep_var prep_propp raw_fixes raw_assumes raw_shows ctxt =
    5.39    let
    5.40 +(**)val _ = writeln "###-# Proof_Context.prep_statement";(**)
    5.41      val ((fixes, (assumes, shows), binds), ctxt') = ctxt
    5.42 -      |> prep_stmt prep_var prep_propp raw_fixes (raw_assumes @ raw_shows)
    5.43 +      |> prep_stmt(*<-----*) prep_var prep_propp raw_fixes (raw_assumes @ raw_shows)
    5.44        |-> (fn {vars, propss, binds, ...} =>
    5.45          fold Variable.bind_term binds #>
    5.46          pair (map #2 vars, chop (length raw_assumes) propss, binds));
    5.47 @@ -1430,7 +1435,13 @@
    5.48  val cert_stmt = prep_stmt cert_var cert_propp;
    5.49  val read_stmt = prep_stmt read_var read_propp;
    5.50  val cert_statement = prep_statement cert_var cert_propp;
    5.51 +val cert_statement =
    5.52 +  ((**)writeln "###-# Proof_Context.cert_statement";(**)
    5.53 +    prep_statement cert_var cert_propp);
    5.54  val read_statement = prep_statement read_var read_propp;
    5.55 +val read_statement =
    5.56 +  ((**)writeln "###-# Proof_Context.read_statement";(**)
    5.57 +    prep_statement read_var read_propp);
    5.58  
    5.59  end;
    5.60  

     6.1 --- a/src/Pure/Isar/specification.ML	Mon Dec 21 15:13:49 2020 +0100
     6.2 +++ b/src/Pure/Isar/specification.ML	Tue Jan 05 17:29:39 2021 +0100
     6.3 @@ -206,6 +206,7 @@
     6.4  
     6.5  fun gen_axioms prep_stmt prep_att raw_decls raw_fixes raw_prems raw_concls thy =
     6.6    let
     6.7 +    val _ = writeln "###-# Specification.gen_axioms";
     6.8      (*specification*)
     6.9      val ({vars, propss = [prems, concls], ...}, vars_ctxt) =
    6.10        Proof_Context.init_global thy

     7.1 --- a/src/Pure/ML/ml_thms.ML	Mon Dec 21 15:13:49 2020 +0100
     7.2 +++ b/src/Pure/ML/ml_thms.ML	Tue Jan 05 17:29:39 2021 +0100
     7.3 @@ -16,7 +16,7 @@
     7.4    val bind_thms: string * thm list -> unit
     7.5  end;
     7.6  
     7.7 -structure ML_Thms: ML_THMS =
     7.8 +structure ML_Thms(**): ML_THMS(**) =
     7.9  struct
    7.10  
    7.11  (* auxiliary data *)
    7.12 @@ -52,6 +52,8 @@
    7.13  
    7.14  (* fact references *)
    7.15  
    7.16 +(*  thm_binding: string -> bool -> thm list -> Proof.context -> (Proof.context ->
    7.17 +      string * string) * Proof.context*)
    7.18  fun thm_binding kind is_single thms ctxt =
    7.19    let
    7.20      val initial = null (get_thmss ctxt);
    7.21 @@ -85,14 +87,13 @@
    7.22        (Parse.position by -- Method.parse -- Scan.option Method.parse)))
    7.23      (fn _ => fn ((is_open, raw_propss), (((_, by_pos), m1), m2)) => fn ctxt =>
    7.24        let
    7.25 -        val _ = (**)writeln "##### ML_Thms Theory.setup 1 thm_binding lemma";(**)
    7.26 +        val _ = (**)writeln "###-# ML_Thms Theory.setup thm_binding lemma";(**)
    7.27          val reports =
    7.28            (by_pos, Markup.keyword1 |> Markup.keyword_properties) ::
    7.29              maps Method.reports_of (m1 :: the_list m2);
    7.30          val _ = Context_Position.reports ctxt reports;
    7.31  
    7.32 -        val _ = (**)writeln "##### ML_Thms Theory.setup 2 thm_binding lemma";(**)
    7.33 -        val propss = burrow (map (rpair []) o Syntax.read_props ctxt) raw_propss;
    7.34 +        val propss = burrow (map (rpair []) o Syntax.read_props(*<-----*) ctxt) raw_propss;
    7.35          val prep_result = Goal.norm_result ctxt #> not is_open ? Thm.close_derivation \<^here>;
    7.36          fun after_qed res goal_ctxt =
    7.37            Proof_Context.put_thms false (Auto_Bind.thisN,

     8.1 --- a/src/Pure/Syntax/syntax.ML	Mon Dec 21 15:13:49 2020 +0100
     8.2 +++ b/src/Pure/Syntax/syntax.ML	Tue Jan 05 17:29:39 2021 +0100
     8.3 @@ -315,8 +315,8 @@
     8.4  val read_typ_global = read_typ o Proof_Context.init_global;
     8.5  val read_term_global = read_term o Proof_Context.init_global;
     8.6  val read_prop_global =
     8.7 -((**)writeln "##### Syntax.read_prop_global";(**)
     8.8 -  read_prop o Proof_Context.init_global);
     8.9 +  ((**)writeln "##### Syntax.read_prop_global";(**)
    8.10 +    read_prop o Proof_Context.init_global);
    8.11  
    8.12  
    8.13  (* pretty = uncheck + unparse *)