| changeset 66259 | b5279a21e658 |
| parent 63402 | f199837304d7 |
| child 66333 | 30c1639a343a |
--- a/src/Pure/Isar/named_target.ML Sat Jul 08 19:34:46 2017 +0200 +++ b/src/Pure/Isar/named_target.ML Sat Jul 08 20:05:26 2017 +0200 @@ -163,7 +163,7 @@ fun begin ("-", _) thy = theory_init thy | begin target thy = init NONE (Locale.check thy target) thy; -val exit = Local_Theory.assert_bottom true #> Local_Theory.exit_global; +val exit = Local_Theory.assert_bottom #> Local_Theory.exit_global; fun switch NONE (Context.Theory thy) = (Context.Theory o exit, theory_init thy)