| changeset 19475 | 8aa2b380614a |
| parent 19423 | 51eeee99bd8f |
| child 19482 | 9f11af8f7ef9 |
--- a/src/Pure/Isar/proof.ML Wed Apr 26 22:38:11 2006 +0200 +++ b/src/Pure/Isar/proof.ML Wed Apr 26 22:38:16 2006 +0200 @@ -892,7 +892,7 @@ fun check_result msg sq = (case Seq.pull sq of NONE => error msg - | SOME res => Seq.cons res); + | SOME (s', sq') => Seq.cons s' sq'); fun global_qeds txt = end_proof true txt