| changeset 23682 | cf4773532006 |
| parent 23676 | ea9b7e9c2301 |
| child 23728 | 8409a0cd5b04 |
--- a/src/Pure/General/symbol.ML Mon Jul 09 23:12:51 2007 +0200 +++ b/src/Pure/General/symbol.ML Tue Jul 10 00:17:52 2007 +0200 @@ -428,7 +428,8 @@ in fun source do_recover src = - Source.source stopper (Scan.bulk scan) (if do_recover then SOME (K recover) else NONE) src; + Source.source stopper (Scan.bulk scan) + (if do_recover then SOME (false, K recover) else NONE) src; end;