# HG changeset patch
# User wenzelm
# Date 1428320062 -7200
# Node ID 74872a13f628c00fc0752d32f6240a39a6a29242
# Parent  5ec4f97dd6d42370089020fbe394dc68191d3e7e
support local command setup;

diff -r 5ec4f97dd6d4 -r 74872a13f628 src/Pure/Isar/outer_syntax.ML
--- a/src/Pure/Isar/outer_syntax.ML	Mon Apr 06 13:28:54 2015 +0200
+++ b/src/Pure/Isar/outer_syntax.ML	Mon Apr 06 13:34:22 2015 +0200
@@ -137,7 +137,8 @@
 type command_spec = string * Position.T;
 
 fun raw_command (name, pos) comment command_parser =
-  Theory.setup (add_command name (new_command comment command_parser pos));
+  let val setup = add_command name (new_command comment command_parser pos)
+  in Context.>> (Context.mapping setup (Local_Theory.background_theory setup)) end;
 
 fun command (name, pos) comment parse =
   raw_command (name, pos) comment (Parser parse);