src/Pure/Isar/named_target.ML
changeset 47274 feef9b0b6031
parent 47251 13a770bd5544
child 47275 fc95b8b6c260
--- a/src/Pure/Isar/named_target.ML	Mon Apr 02 17:00:32 2012 +0200
+++ b/src/Pure/Isar/named_target.ML	Mon Apr 02 19:10:52 2012 +0200
@@ -192,7 +192,7 @@
   Local_Theory.assert_bottom true #> Data.get #> the #>
   (fn Target {target, before_exit, ...} => Local_Theory.exit_global #> init before_exit target);
 
-fun context_cmd ("-", _) thy = init I "" thy
+fun context_cmd ("-", _) thy = theory_init thy
   | context_cmd target thy = init I (Locale.check thy target) thy;
 
 end;