src/Pure/Isar/obtain.ML
changeset 60138 209f8c177b5b
parent 60065 46266dc209cd
child 60139 c3cb65678c47
     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