1.1 --- a/src/Pure/Thy/thy_edit.ML	Tue Sep 30 23:31:38 2008 +0200
     1.2 +++ b/src/Pure/Thy/thy_edit.ML	Tue Sep 30 23:31:40 2008 +0200
     1.3 @@ -24,7 +24,7 @@
     1.4    val present_span: span -> output
     1.5    val report_span: span -> unit
     1.6    val unit_source: (span, 'a) Source.source ->
     1.7 -    (span * span list, (span, 'a) Source.source) Source.source
     1.8 +    (span * span list * bool, (span, 'a) Source.source) Source.source
     1.9  end;
    1.10  
    1.11  structure ThyEdit: THY_EDIT =
    1.12 @@ -179,9 +179,11 @@
    1.13      command_with K.is_proof_goal >> pair (d + 1) ||
    1.14      (if d <= 1 then Scan.fail else command_with K.is_qed >> pair (d - 1)) ||
    1.15      command_with K.is_qed_global >> pair 0 ||
    1.16 -    Scan.unless (command_with K.is_theory) (Scan.one not_eof) >> pair d)));
    1.17 +    Scan.unless (command_with K.is_theory) (Scan.one not_eof) >> pair d)) -- Scan.state);
    1.18  
    1.19 -val unit = command_with K.is_theory_goal -- proof || Scan.one not_eof >> rpair [];
    1.20 +val unit =
    1.21 +  command_with K.is_theory_goal -- proof >> (fn (a, (bs, d)) => (a, bs, d <> 0)) ||
    1.22 +  Scan.one not_eof >> (fn a => (a, [], true));
    1.23  
    1.24  in
    1.25