1.1 --- a/src/Pure/Isar/obtain.ML Thu Dec 17 11:45:12 2020 +0100
1.2 +++ b/src/Pure/Isar/obtain.ML Thu Dec 17 18:00:27 2020 +0100
1.3 @@ -131,9 +131,11 @@
1.4 val parse_clause = prepare_clause Proof_Context.read_var Syntax.parse_prop mk_all_external;
1.5 val cert_clause = prepare_clause Proof_Context.cert_var (K I) mk_all_internal;
1.6
1.7 -in
1.8 +in
1.9
1.10 -val read_obtains = prepare_obtains parse_clause Syntax.check_terms;
1.11 +val read_obtains =
1.12 + (writeln "#### Obtain.read_obtains";
1.13 + prepare_obtains parse_clause Syntax.check_terms);
1.14 val cert_obtains = prepare_obtains cert_clause (K I);
1.15 val parse_obtains = prepare_obtains parse_clause (K I);
1.16