# HG changeset patch
# User wenzelm
# Date 1428317485 -7200
# Node ID bdbc4b761c319ba96112ea7f5c3653d9a02bb30f
# Parent  a090551e5ec8fbd37e0153ea1d0713b86d27d57f
tuned signature;

diff -r a090551e5ec8 -r bdbc4b761c31 src/Pure/Isar/isar_cmd.ML
--- a/src/Pure/Isar/isar_cmd.ML	Mon Apr 06 12:37:21 2015 +0200
+++ b/src/Pure/Isar/isar_cmd.ML	Mon Apr 06 12:51:25 2015 +0200
@@ -6,7 +6,7 @@
 
 signature ISAR_CMD =
 sig
-  val global_setup: Input.source -> theory -> theory
+  val setup: Input.source -> theory -> theory
   val local_setup: Input.source -> Proof.context -> Proof.context
   val parse_ast_translation: Input.source -> theory -> theory
   val parse_translation: Input.source -> theory -> theory
@@ -57,7 +57,7 @@
 
 (* generic setup *)
 
-fun global_setup source =
+fun setup source =
   ML_Lex.read_source false source
   |> ML_Context.expression (Input.range_of source) "setup" "theory -> theory"
     "Context.map_theory setup"
diff -r a090551e5ec8 -r bdbc4b761c31 src/Pure/Isar/isar_syn.ML
--- a/src/Pure/Isar/isar_syn.ML	Mon Apr 06 12:37:21 2015 +0200
+++ b/src/Pure/Isar/isar_syn.ML	Mon Apr 06 12:51:25 2015 +0200
@@ -257,11 +257,11 @@
     (Parse.ML_source >> Isar_Cmd.ml_diag false);
 
 val _ =
-  Outer_Syntax.command @{command_spec "setup"} "ML theory setup"
-    (Parse.ML_source >> (Toplevel.theory o Isar_Cmd.global_setup));
+  Outer_Syntax.command @{command_spec "setup"} "ML setup for global theory"
+    (Parse.ML_source >> (Toplevel.theory o Isar_Cmd.setup));
 
 val _ =
-  Outer_Syntax.local_theory @{command_spec "local_setup"} "ML local theory setup"
+  Outer_Syntax.local_theory @{command_spec "local_setup"} "ML setup for local theory"
     (Parse.ML_source >> Isar_Cmd.local_setup);
 
 val _ =
@@ -913,4 +913,3 @@
         Toplevel.end_proof (K Proof.end_notepad)));
 
 end;
-
diff -r a090551e5ec8 -r bdbc4b761c31 src/Pure/theory.ML
--- a/src/Pure/theory.ML	Mon Apr 06 12:37:21 2015 +0200
+++ b/src/Pure/theory.ML	Mon Apr 06 12:51:25 2015 +0200
@@ -14,6 +14,7 @@
   val merge: theory * theory -> theory
   val merge_list: theory list -> theory
   val setup: (theory -> theory) -> unit
+  val local_setup: (Proof.context -> Proof.context) -> unit
   val get_markup: theory -> Markup.T
   val axiom_table: theory -> term Name_Space.table
   val axiom_space: theory -> Name_Space.T
@@ -51,6 +52,7 @@
   | merge_list (thy :: thys) = Library.foldl merge (thy, thys);
 
 fun setup f = Context.>> (Context.map_theory f);
+fun local_setup f = Context.>> (Context.map_proof f);