--- a/src/Pure/Isar/named_target.ML Fri Feb 26 22:38:44 2016 +0100
+++ b/src/Pure/Isar/named_target.ML Sat Mar 05 12:49:47 2016 +0100
@@ -176,7 +176,7 @@
| switch (SOME name) (Context.Theory thy) =
(Context.Theory o exit, begin name thy)
| switch NONE (Context.Proof lthy) =
- (Context.Proof o Local_Theory.restore, lthy)
+ (Context.Proof o Local_Theory.reset, lthy)
| switch (SOME name) (Context.Proof lthy) =
(Context.Proof o init (target_of lthy) o exit,
(begin name o exit o Local_Theory.assert_nonbrittle) lthy);