1.1 --- a/src/FOL/FOL.thy	Mon Jun 27 15:03:55 2011 +0200
     1.2 +++ b/src/FOL/FOL.thy	Mon Jun 27 16:53:31 2011 +0200
     1.3 @@ -177,12 +177,15 @@
     1.4    val hyp_subst_tacs = [hyp_subst_tac]
     1.5  );
     1.6  
     1.7 -ML_Antiquote.value "claset" (Scan.succeed "Cla.claset_of (ML_Context.the_local_context ())");
     1.8 -
     1.9  structure Basic_Classical: BASIC_CLASSICAL = Cla;
    1.10  open Basic_Classical;
    1.11  *}
    1.12  
    1.13 +setup {*
    1.14 +  ML_Antiquote.value @{binding claset}
    1.15 +    (Scan.succeed "Cla.claset_of (ML_Context.the_local_context ())")
    1.16 +*}
    1.17 +
    1.18  setup Cla.setup
    1.19  
    1.20  (*Propositional rules*)

     2.1 --- a/src/HOL/HOL.thy	Mon Jun 27 15:03:55 2011 +0200
     2.2 +++ b/src/HOL/HOL.thy	Mon Jun 27 16:53:31 2011 +0200
     2.3 @@ -853,9 +853,11 @@
     2.4  
     2.5  structure Basic_Classical: BASIC_CLASSICAL = Classical; 
     2.6  open Basic_Classical;
     2.7 +*}
     2.8  
     2.9 -ML_Antiquote.value "claset"
    2.10 -  (Scan.succeed "Classical.claset_of (ML_Context.the_local_context ())");
    2.11 +setup {*
    2.12 +  ML_Antiquote.value @{binding claset}
    2.13 +    (Scan.succeed "Classical.claset_of (ML_Context.the_local_context ())")
    2.14  *}
    2.15  
    2.16  setup Classical.setup

     3.1 --- a/src/Pure/General/markup.ML	Mon Jun 27 15:03:55 2011 +0200
     3.2 +++ b/src/Pure/General/markup.ML	Mon Jun 27 16:53:31 2011 +0200
     3.3 @@ -72,7 +72,7 @@
     3.4    val ML_sourceN: string val ML_source: T
     3.5    val doc_sourceN: string val doc_source: T
     3.6    val antiqN: string val antiq: T
     3.7 -  val ML_antiqN: string val ML_antiq: string -> T
     3.8 +  val ML_antiquotationN: string
     3.9    val doc_antiqN: string val doc_antiq: string -> T
    3.10    val keyword_declN: string val keyword_decl: string -> T
    3.11    val command_declN: string val command_decl: string -> string -> T
    3.12 @@ -266,7 +266,7 @@
    3.13  val (doc_sourceN, doc_source) = markup_elem "doc_source";
    3.14  
    3.15  val (antiqN, antiq) = markup_elem "antiq";
    3.16 -val (ML_antiqN, ML_antiq) = markup_string "ML_antiq" nameN;
    3.17 +val ML_antiquotationN = "ML antiquotation";
    3.18  val (doc_antiqN, doc_antiq) = markup_string "doc_antiq" nameN;
    3.19  
    3.20  

     4.1 --- a/src/Pure/General/markup.scala	Mon Jun 27 15:03:55 2011 +0200
     4.2 +++ b/src/Pure/General/markup.scala	Mon Jun 27 16:53:31 2011 +0200
     4.3 @@ -189,7 +189,7 @@
     4.4    val DOC_SOURCE = "doc_source"
     4.5  
     4.6    val ANTIQ = "antiq"
     4.7 -  val ML_ANTIQ = "ML_antiq"
     4.8 +  val ML_ANTIQUOTATION = "ML antiquotation"
     4.9    val DOC_ANTIQ = "doc_antiq"
    4.10  
    4.11  

     5.1 --- a/src/Pure/General/name_space.ML	Mon Jun 27 15:03:55 2011 +0200
     5.2 +++ b/src/Pure/General/name_space.ML	Mon Jun 27 16:53:31 2011 +0200
     5.3 @@ -50,7 +50,7 @@
     5.4    val declare: Proof.context -> bool -> naming -> binding -> T -> string * T
     5.5    val alias: naming -> binding -> string -> T -> T
     5.6    type 'a table = T * 'a Symtab.table
     5.7 -  val check: Proof.context -> 'a table -> xstring * Position.T -> string
     5.8 +  val check: Proof.context -> 'a table -> xstring * Position.T -> string * 'a
     5.9    val get: 'a table -> string -> 'a
    5.10    val define: Proof.context -> bool -> naming -> binding * 'a -> 'a table -> string * 'a table
    5.11    val empty_table: string -> 'a table
    5.12 @@ -383,15 +383,15 @@
    5.13  
    5.14  
    5.15  
    5.16 -(** name spaces coupled with symbol tables **)
    5.17 +(** name space coupled with symbol table **)
    5.18  
    5.19  type 'a table = T * 'a Symtab.table;
    5.20  
    5.21  fun check ctxt (space, tab) (xname, pos) =
    5.22    let val name = intern space xname in
    5.23 -    if Symtab.defined tab name
    5.24 -    then (Context_Position.report ctxt pos (markup space name); name)
    5.25 -    else error (undefined (kind_of space) name ^ Position.str_of pos)
    5.26 +    (case Symtab.lookup tab name of
    5.27 +      SOME x => (Context_Position.report ctxt pos (markup space name); (name, x))
    5.28 +    | NONE => error (undefined (kind_of space) name ^ Position.str_of pos))
    5.29    end;
    5.30  
    5.31  fun get (space, tab) name =

     6.1 --- a/src/Pure/Isar/isar_cmd.ML	Mon Jun 27 15:03:55 2011 +0200
     6.2 +++ b/src/Pure/Isar/isar_cmd.ML	Mon Jun 27 16:53:31 2011 +0200
     6.3 @@ -303,8 +303,12 @@
     6.4    Proof.goal (Toplevel.proof_of (diag_state ()))
     6.5      handle Toplevel.UNDEF => error "No goal present";
     6.6  
     6.7 -val _ = ML_Antiquote.value "Isar.state" (Scan.succeed "Isar_Cmd.diag_state ()");
     6.8 -val _ = ML_Antiquote.value "Isar.goal" (Scan.succeed "Isar_Cmd.diag_goal ()");
     6.9 +val _ =
    6.10 +  Context.>> (Context.map_theory
    6.11 +   (ML_Antiquote.value (Binding.qualify true "Isar" (Binding.name "state"))
    6.12 +      (Scan.succeed "Isar_Cmd.diag_state ()") #>
    6.13 +    ML_Antiquote.value (Binding.qualify true "Isar" (Binding.name "goal"))
    6.14 +      (Scan.succeed "Isar_Cmd.diag_goal ()")));
    6.15  
    6.16  
    6.17  (* present draft files *)

     7.1 --- a/src/Pure/ML/ml_antiquote.ML	Mon Jun 27 15:03:55 2011 +0200
     7.2 +++ b/src/Pure/ML/ml_antiquote.ML	Mon Jun 27 16:53:31 2011 +0200
     7.3 @@ -6,11 +6,11 @@
     7.4  
     7.5  signature ML_ANTIQUOTE =
     7.6  sig
     7.7 -  val macro: string -> Proof.context context_parser -> unit
     7.8    val variant: string -> Proof.context -> string * Proof.context
     7.9 -  val inline: string -> string context_parser -> unit
    7.10 -  val declaration: string -> string -> string context_parser -> unit
    7.11 -  val value: string -> string context_parser -> unit
    7.12 +  val macro: binding -> Proof.context context_parser -> theory -> theory
    7.13 +  val inline: binding -> string context_parser -> theory -> theory
    7.14 +  val declaration: string -> binding -> string context_parser -> theory -> theory
    7.15 +  val value: binding -> string context_parser -> theory -> theory
    7.16  end;
    7.17  
    7.18  structure ML_Antiquote: ML_ANTIQUOTE =
    7.19 @@ -46,7 +46,8 @@
    7.20  fun declaration kind name scan = ML_Context.add_antiq name
    7.21    (fn _ => scan >> (fn s => fn background =>
    7.22      let
    7.23 -      val (a, background') = variant (translate_string (fn "." => "_" | c => c) name) background;
    7.24 +      val (a, background') =
    7.25 +        variant (translate_string (fn "." => "_" | c => c) (Binding.name_of name)) background;
    7.26        val env = kind ^ " " ^ a ^ " = " ^ s ^ ";\n";
    7.27        val body = "Isabelle." ^ a;
    7.28      in (K (env, body), background') end));
    7.29 @@ -57,48 +58,55 @@
    7.30  
    7.31  (** misc antiquotations **)
    7.32  
    7.33 -val _ = inline "assert"
    7.34 -  (Scan.succeed "(fn b => if b then () else raise General.Fail \"Assertion failed\")");
    7.35 +val _ = Context.>> (Context.map_theory
    7.36  
    7.37 -val _ = inline "make_string" (Scan.succeed ml_make_string);
    7.38 + (inline (Binding.name "assert")
    7.39 +    (Scan.succeed "(fn b => if b then () else raise General.Fail \"Assertion failed\")") #>
    7.40  
    7.41 -val _ = value "binding"
    7.42 -  (Scan.lift (Parse.position Args.name)
    7.43 -    >> (fn name => ML_Syntax.atomic (ML_Syntax.make_binding name)));
    7.44 +  inline (Binding.name "make_string") (Scan.succeed ml_make_string) #>
    7.45  
    7.46 -val _ = value "theory"
    7.47 -  (Scan.lift Args.name >> (fn name =>
    7.48 -    "Context.get_theory (ML_Context.the_global_context ()) " ^ ML_Syntax.print_string name)
    7.49 -  || Scan.succeed "ML_Context.the_global_context ()");
    7.50 +  value (Binding.name "binding")
    7.51 +    (Scan.lift (Parse.position Args.name)
    7.52 +      >> (fn name => ML_Syntax.atomic (ML_Syntax.make_binding name))) #>
    7.53  
    7.54 -val _ = value "context" (Scan.succeed "ML_Context.the_local_context ()");
    7.55 +  value (Binding.name "theory")
    7.56 +    (Scan.lift Args.name >> (fn name =>
    7.57 +      "Context.get_theory (ML_Context.the_global_context ()) " ^ ML_Syntax.print_string name)
    7.58 +    || Scan.succeed "ML_Context.the_global_context ()") #>
    7.59  
    7.60 -val _ = inline "typ" (Args.typ >> (ML_Syntax.atomic o ML_Syntax.print_typ));
    7.61 -val _ = inline "term" (Args.term >> (ML_Syntax.atomic o ML_Syntax.print_term));
    7.62 -val _ = inline "prop" (Args.prop >> (ML_Syntax.atomic o ML_Syntax.print_term));
    7.63 +  value (Binding.name "context") (Scan.succeed "ML_Context.the_local_context ()") #>
    7.64  
    7.65 -val _ = macro "let" (Args.context --
    7.66 -  Scan.lift
    7.67 -    (Parse.and_list1 (Parse.and_list1 Args.name_source -- (Args.$$$ "=" |-- Args.name_source)))
    7.68 -    >> (fn (ctxt, args) => #2 (Proof_Context.match_bind true args ctxt)));
    7.69 +  inline (Binding.name "typ") (Args.typ >> (ML_Syntax.atomic o ML_Syntax.print_typ)) #>
    7.70 +  inline (Binding.name "term") (Args.term >> (ML_Syntax.atomic o ML_Syntax.print_term)) #>
    7.71 +  inline (Binding.name "prop") (Args.prop >> (ML_Syntax.atomic o ML_Syntax.print_term)) #>
    7.72  
    7.73 -val _ = macro "note" (Args.context :|-- (fn ctxt =>
    7.74 -  Parse.and_list1' (Scan.lift (Args.opt_thm_name I "=") -- Attrib.thms >> (fn ((a, srcs), ths) =>
    7.75 -    ((a, map (Attrib.attribute (Proof_Context.theory_of ctxt)) srcs), [(ths, [])])))
    7.76 -  >> (fn args => #2 (Proof_Context.note_thmss "" args ctxt))));
    7.77 +  macro (Binding.name "let")
    7.78 +    (Args.context --
    7.79 +      Scan.lift
    7.80 +        (Parse.and_list1 (Parse.and_list1 Args.name_source -- (Args.$$$ "=" |-- Args.name_source)))
    7.81 +        >> (fn (ctxt, args) => #2 (Proof_Context.match_bind true args ctxt))) #>
    7.82  
    7.83 -val _ = value "ctyp" (Args.typ >> (fn T =>
    7.84 -  "Thm.ctyp_of (ML_Context.the_global_context ()) " ^ ML_Syntax.atomic (ML_Syntax.print_typ T)));
    7.85 +  macro (Binding.name "note")
    7.86 +    (Args.context :|-- (fn ctxt =>
    7.87 +      Parse.and_list1' (Scan.lift (Args.opt_thm_name I "=") -- Attrib.thms
    7.88 +        >> (fn ((a, srcs), ths) =>
    7.89 +          ((a, map (Attrib.attribute (Proof_Context.theory_of ctxt)) srcs), [(ths, [])])))
    7.90 +      >> (fn args => #2 (Proof_Context.note_thmss "" args ctxt)))) #>
    7.91  
    7.92 -val _ = value "cterm" (Args.term >> (fn t =>
    7.93 -  "Thm.cterm_of (ML_Context.the_global_context ()) " ^ ML_Syntax.atomic (ML_Syntax.print_term t)));
    7.94 +  value (Binding.name "ctyp") (Args.typ >> (fn T =>
    7.95 +    "Thm.ctyp_of (ML_Context.the_global_context ()) " ^ ML_Syntax.atomic (ML_Syntax.print_typ T))) #>
    7.96  
    7.97 -val _ = value "cprop" (Args.prop >> (fn t =>
    7.98 -  "Thm.cterm_of (ML_Context.the_global_context ()) " ^ ML_Syntax.atomic (ML_Syntax.print_term t)));
    7.99 +  value (Binding.name "cterm") (Args.term >> (fn t =>
   7.100 +  "Thm.cterm_of (ML_Context.the_global_context ()) " ^ ML_Syntax.atomic (ML_Syntax.print_term t))) #>
   7.101  
   7.102 -val _ = value "cpat"
   7.103 -  (Args.context -- Scan.lift Args.name_source >> uncurry Proof_Context.read_term_pattern >> (fn t =>
   7.104 -    "Thm.cterm_of (ML_Context.the_global_context ()) " ^ ML_Syntax.atomic (ML_Syntax.print_term t)));
   7.105 +  value (Binding.name "cprop") (Args.prop >> (fn t =>
   7.106 +  "Thm.cterm_of (ML_Context.the_global_context ()) " ^ ML_Syntax.atomic (ML_Syntax.print_term t))) #>
   7.107 +
   7.108 +  value (Binding.name "cpat")
   7.109 +    (Args.context --
   7.110 +      Scan.lift Args.name_source >> uncurry Proof_Context.read_term_pattern >> (fn t =>
   7.111 +        "Thm.cterm_of (ML_Context.the_global_context ()) " ^
   7.112 +          ML_Syntax.atomic (ML_Syntax.print_term t)))));
   7.113  
   7.114  
   7.115  (* type classes *)
   7.116 @@ -108,11 +116,13 @@
   7.117    |> syn ? Lexicon.mark_class
   7.118    |> ML_Syntax.print_string);
   7.119  
   7.120 -val _ = inline "class" (class false);
   7.121 -val _ = inline "class_syntax" (class true);
   7.122 +val _ = Context.>> (Context.map_theory
   7.123 + (inline (Binding.name "class") (class false) #>
   7.124 +  inline (Binding.name "class_syntax") (class true) #>
   7.125  
   7.126 -val _ = inline "sort" (Args.context -- Scan.lift Args.name_source >> (fn (ctxt, s) =>
   7.127 -  ML_Syntax.atomic (ML_Syntax.print_sort (Syntax.read_sort ctxt s))));
   7.128 +  inline (Binding.name "sort")
   7.129 +    (Args.context -- Scan.lift Args.name_source >> (fn (ctxt, s) =>
   7.130 +      ML_Syntax.atomic (ML_Syntax.print_sort (Syntax.read_sort ctxt s))))));
   7.131  
   7.132  
   7.133  (* type constructors *)
   7.134 @@ -128,10 +138,15 @@
   7.135          | NONE => error ("Not a " ^ kind ^ ": " ^ quote c ^ Position.str_of pos));
   7.136      in ML_Syntax.print_string res end);
   7.137  
   7.138 -val _ = inline "type_name" (type_name "logical type" (fn (c, Type.LogicalType _) => c));
   7.139 -val _ = inline "type_abbrev" (type_name "type abbreviation" (fn (c, Type.Abbreviation _) => c));
   7.140 -val _ = inline "nonterminal" (type_name "nonterminal" (fn (c, Type.Nonterminal) => c));
   7.141 -val _ = inline "type_syntax" (type_name "type" (fn (c, _) => Lexicon.mark_type c));
   7.142 +val _ = Context.>> (Context.map_theory
   7.143 + (inline (Binding.name "type_name")
   7.144 +    (type_name "logical type" (fn (c, Type.LogicalType _) => c)) #>
   7.145 +  inline (Binding.name "type_abbrev")
   7.146 +    (type_name "type abbreviation" (fn (c, Type.Abbreviation _) => c)) #>
   7.147 +  inline (Binding.name "nonterminal")
   7.148 +    (type_name "nonterminal" (fn (c, Type.Nonterminal) => c)) #>
   7.149 +  inline (Binding.name "type_syntax")
   7.150 +    (type_name "type" (fn (c, _) => Lexicon.mark_type c))));
   7.151  
   7.152  
   7.153  (* constants *)
   7.154 @@ -144,25 +159,28 @@
   7.155          handle TYPE (msg, _, _) => error (msg ^ Position.str_of pos);
   7.156      in ML_Syntax.print_string res end);
   7.157  
   7.158 -val _ = inline "const_name" (const_name (fn (consts, c) => (Consts.the_type consts c; c)));
   7.159 -val _ = inline "const_abbrev" (const_name (fn (consts, c) => (Consts.the_abbreviation consts c; c)));
   7.160 -val _ = inline "const_syntax" (const_name (fn (_, c) => Lexicon.mark_const c));
   7.161 +val _ = Context.>> (Context.map_theory
   7.162 + (inline (Binding.name "const_name")
   7.163 +    (const_name (fn (consts, c) => (Consts.the_type consts c; c))) #>
   7.164 +  inline (Binding.name "const_abbrev")
   7.165 +    (const_name (fn (consts, c) => (Consts.the_abbreviation consts c; c))) #>
   7.166 +  inline (Binding.name "const_syntax")
   7.167 +    (const_name (fn (_, c) => Lexicon.mark_const c)) #>
   7.168  
   7.169 +  inline (Binding.name "syntax_const")
   7.170 +    (Args.context -- Scan.lift (Parse.position Args.name) >> (fn (ctxt, (c, pos)) =>
   7.171 +      if is_some (Syntax.lookup_const (Proof_Context.syn_of ctxt) c)
   7.172 +      then ML_Syntax.print_string c
   7.173 +      else error ("Unknown syntax const: " ^ quote c ^ Position.str_of pos))) #>
   7.174  
   7.175 -val _ = inline "syntax_const"
   7.176 -  (Args.context -- Scan.lift (Parse.position Args.name) >> (fn (ctxt, (c, pos)) =>
   7.177 -    if is_some (Syntax.lookup_const (Proof_Context.syn_of ctxt) c)
   7.178 -    then ML_Syntax.print_string c
   7.179 -    else error ("Unknown syntax const: " ^ quote c ^ Position.str_of pos)));
   7.180 -
   7.181 -val _ = inline "const"
   7.182 -  (Args.context -- Scan.lift Args.name_source -- Scan.optional
   7.183 -      (Scan.lift (Args.$$$ "(") |-- Parse.enum1' "," Args.typ --| Scan.lift (Args.$$$ ")")) []
   7.184 -    >> (fn ((ctxt, raw_c), Ts) =>
   7.185 -      let
   7.186 -        val Const (c, _) = Proof_Context.read_const_proper ctxt true raw_c;
   7.187 -        val const = Const (c, Consts.instance (Proof_Context.consts_of ctxt) (c, Ts));
   7.188 -      in ML_Syntax.atomic (ML_Syntax.print_term const) end));
   7.189 +  inline (Binding.name "const")
   7.190 +    (Args.context -- Scan.lift Args.name_source -- Scan.optional
   7.191 +        (Scan.lift (Args.$$$ "(") |-- Parse.enum1' "," Args.typ --| Scan.lift (Args.$$$ ")")) []
   7.192 +      >> (fn ((ctxt, raw_c), Ts) =>
   7.193 +        let
   7.194 +          val Const (c, _) = Proof_Context.read_const_proper ctxt true raw_c;
   7.195 +          val const = Const (c, Consts.instance (Proof_Context.consts_of ctxt) (c, Ts));
   7.196 +        in ML_Syntax.atomic (ML_Syntax.print_term const) end))));
   7.197  
   7.198  end;
   7.199  

     8.1 --- a/src/Pure/ML/ml_context.ML	Mon Jun 27 15:03:55 2011 +0200
     8.2 +++ b/src/Pure/ML/ml_context.ML	Mon Jun 27 16:53:31 2011 +0200
     8.3 @@ -24,7 +24,7 @@
     8.4    val ml_store_thms: string * thm list -> unit
     8.5    val ml_store_thm: string * thm -> unit
     8.6    type antiq = Proof.context -> (Proof.context -> string * string) * Proof.context
     8.7 -  val add_antiq: string -> (Position.T -> antiq context_parser) -> unit
     8.8 +  val add_antiq: binding -> (Position.T -> antiq context_parser) -> theory -> theory
     8.9    val trace_raw: Config.raw
    8.10    val trace: bool Config.T
    8.11    val eval_antiquotes: ML_Lex.token Antiquote.antiquote list * Position.T ->
    8.12 @@ -99,29 +99,25 @@
    8.13  
    8.14  type antiq = Proof.context -> (Proof.context -> string * string) * Proof.context;
    8.15  
    8.16 -local
    8.17 +structure Antiq_Parsers = Theory_Data
    8.18 +(
    8.19 +  type T = (Position.T -> antiq context_parser) Name_Space.table;
    8.20 +  val empty : T = Name_Space.empty_table Markup.ML_antiquotationN;
    8.21 +  val extend = I;
    8.22 +  fun merge data : T = Name_Space.merge_tables data;
    8.23 +);
    8.24  
    8.25 -val global_parsers =
    8.26 -  Unsynchronized.ref (Symtab.empty: (Position.T -> antiq context_parser) Symtab.table);
    8.27 -
    8.28 -in
    8.29 -
    8.30 -fun add_antiq name scan = CRITICAL (fn () =>
    8.31 -  Unsynchronized.change global_parsers (fn tab =>
    8.32 -   (if not (Symtab.defined tab name) then ()
    8.33 -    else warning ("Redefined ML antiquotation: " ^ quote name);
    8.34 -    Symtab.update (name, scan) tab)));
    8.35 +fun add_antiq name scan thy = thy
    8.36 +  |> Antiq_Parsers.map
    8.37 +    (Name_Space.define (Proof_Context.init_global thy) true (Sign.naming_of thy)
    8.38 +      (name, scan) #> snd);
    8.39  
    8.40  fun antiquotation src ctxt =
    8.41 -  let val ((name, _), pos) = Args.dest_src src in
    8.42 -    (case Symtab.lookup (! global_parsers) name of
    8.43 -      NONE => error ("Unknown ML antiquotation command: " ^ quote name ^ Position.str_of pos)
    8.44 -    | SOME scan =>
    8.45 -       (Context_Position.report ctxt pos (Markup.ML_antiq name);
    8.46 -        Args.context_syntax "ML antiquotation" (scan pos) src ctxt))
    8.47 -  end;
    8.48 -
    8.49 -end;
    8.50 +  let
    8.51 +    val thy = Proof_Context.theory_of ctxt;
    8.52 +    val ((xname, _), pos) = Args.dest_src src;
    8.53 +    val (_, scan) = Name_Space.check ctxt (Antiq_Parsers.get thy) (xname, pos);
    8.54 +  in Args.context_syntax Markup.ML_antiquotationN (scan pos) src ctxt end;
    8.55  
    8.56  
    8.57  (* parsing and evaluation *)

     9.1 --- a/src/Pure/ML/ml_thms.ML	Mon Jun 27 15:03:55 2011 +0200
     9.2 +++ b/src/Pure/ML/ml_thms.ML	Mon Jun 27 16:53:31 2011 +0200
     9.3 @@ -33,7 +33,7 @@
     9.4  
     9.5  (* fact references *)
     9.6  
     9.7 -fun thm_antiq kind scan = ML_Context.add_antiq kind
     9.8 +fun thm_antiq kind scan = ML_Context.add_antiq (Binding.name kind)
     9.9    (fn _ => scan >> (fn ths => fn background =>
    9.10      let
    9.11        val i = serial ();
    9.12 @@ -42,8 +42,10 @@
    9.13        val ml = (thm_bind kind a i, "Isabelle." ^ a);
    9.14      in (K ml, background') end));
    9.15  
    9.16 -val _ = thm_antiq "thm" (Attrib.thm >> single);
    9.17 -val _ = thm_antiq "thms" Attrib.thms;
    9.18 +val _ =
    9.19 +  Context.>> (Context.map_theory
    9.20 +   (thm_antiq "thm" (Attrib.thm >> single) #>
    9.21 +    thm_antiq "thms" Attrib.thms));
    9.22  
    9.23  
    9.24  (* ad-hoc goals *)
    9.25 @@ -52,25 +54,27 @@
    9.26  val by = Args.$$$ "by";
    9.27  val goal = Scan.unless (by || and_) Args.name;
    9.28  
    9.29 -val _ = ML_Context.add_antiq "lemma"
    9.30 -  (fn _ => Args.context -- Args.mode "open" --
    9.31 -      Scan.lift (Parse.and_list1 (Scan.repeat1 goal) --
    9.32 -        (by |-- Method.parse -- Scan.option Method.parse)) >>
    9.33 -    (fn ((ctxt, is_open), (raw_propss, methods)) => fn background =>
    9.34 -      let
    9.35 -        val propss = burrow (map (rpair []) o Syntax.read_props ctxt) raw_propss;
    9.36 -        val i = serial ();
    9.37 -        val prep_result = Goal.norm_result #> not is_open ? Thm.close_derivation;
    9.38 -        fun after_qed res goal_ctxt =
    9.39 -          put_thms (i, map prep_result (Proof_Context.export goal_ctxt ctxt (flat res))) goal_ctxt;
    9.40 -        val ctxt' = ctxt
    9.41 -          |> Proof.theorem NONE after_qed propss
    9.42 -          |> Proof.global_terminal_proof methods;
    9.43 -        val (a, background') = background
    9.44 -          |> ML_Antiquote.variant "lemma" ||> put_thms (i, the_thms ctxt' i);
    9.45 -        val ml =
    9.46 -          (thm_bind (if length (flat propss) = 1 then "thm" else "thms") a i, "Isabelle." ^ a);
    9.47 -      in (K ml, background') end));
    9.48 +val _ =
    9.49 +  Context.>> (Context.map_theory
    9.50 +   (ML_Context.add_antiq (Binding.name "lemma")
    9.51 +    (fn _ => Args.context -- Args.mode "open" --
    9.52 +        Scan.lift (Parse.and_list1 (Scan.repeat1 goal) --
    9.53 +          (by |-- Method.parse -- Scan.option Method.parse)) >>
    9.54 +      (fn ((ctxt, is_open), (raw_propss, methods)) => fn background =>
    9.55 +        let
    9.56 +          val propss = burrow (map (rpair []) o Syntax.read_props ctxt) raw_propss;
    9.57 +          val i = serial ();
    9.58 +          val prep_result = Goal.norm_result #> not is_open ? Thm.close_derivation;
    9.59 +          fun after_qed res goal_ctxt =
    9.60 +            put_thms (i, map prep_result (Proof_Context.export goal_ctxt ctxt (flat res))) goal_ctxt;
    9.61 +          val ctxt' = ctxt
    9.62 +            |> Proof.theorem NONE after_qed propss
    9.63 +            |> Proof.global_terminal_proof methods;
    9.64 +          val (a, background') = background
    9.65 +            |> ML_Antiquote.variant "lemma" ||> put_thms (i, the_thms ctxt' i);
    9.66 +          val ml =
    9.67 +            (thm_bind (if length (flat propss) = 1 then "thm" else "thms") a i, "Isabelle." ^ a);
    9.68 +        in (K ml, background') end))));
    9.69  
    9.70  end;
    9.71  

    10.1 --- a/src/Pure/simplifier.ML	Mon Jun 27 15:03:55 2011 +0200
    10.2 +++ b/src/Pure/simplifier.ML	Mon Jun 27 16:53:31 2011 +0200
    10.3 @@ -139,8 +139,9 @@
    10.4  fun map_simpset f = Context.proof_map (map_ss f);
    10.5  fun simpset_of ctxt = Raw_Simplifier.context ctxt (get_ss (Context.Proof ctxt));
    10.6  
    10.7 -val _ = ML_Antiquote.value "simpset"
    10.8 -  (Scan.succeed "Simplifier.simpset_of (ML_Context.the_local_context ())");
    10.9 +val _ = Context.>> (Context.map_theory
   10.10 +  (ML_Antiquote.value (Binding.name "simpset")
   10.11 +    (Scan.succeed "Simplifier.simpset_of (ML_Context.the_local_context ())")));
   10.12  
   10.13  
   10.14  (* global simpset *)
   10.15 @@ -158,15 +159,16 @@
   10.16  
   10.17  (* get simprocs *)
   10.18  
   10.19 -fun check_simproc ctxt = Name_Space.check ctxt (get_simprocs ctxt);
   10.20 +fun check_simproc ctxt = Name_Space.check ctxt (get_simprocs ctxt) #> #1;
   10.21  val the_simproc = Name_Space.get o get_simprocs;
   10.22  
   10.23  val _ =
   10.24 -  ML_Antiquote.value "simproc"
   10.25 -    (Args.context -- Scan.lift (Parse.position Args.name)
   10.26 -      >> (fn (ctxt, name) =>
   10.27 -        "Simplifier.the_simproc (ML_Context.the_local_context ()) " ^
   10.28 -          ML_Syntax.print_string (check_simproc ctxt name)));
   10.29 +  Context.>> (Context.map_theory
   10.30 +   (ML_Antiquote.value (Binding.name "simproc")
   10.31 +      (Args.context -- Scan.lift (Parse.position Args.name)
   10.32 +        >> (fn (ctxt, name) =>
   10.33 +          "Simplifier.the_simproc (ML_Context.the_local_context ()) " ^
   10.34 +            ML_Syntax.print_string (check_simproc ctxt name)))));
   10.35  
   10.36  
   10.37  (* define simprocs *)

    11.1 --- a/src/Tools/Code/code_runtime.ML	Mon Jun 27 15:03:55 2011 +0200
    11.2 +++ b/src/Tools/Code/code_runtime.ML	Mon Jun 27 16:53:31 2011 +0200
    11.3 @@ -336,7 +336,9 @@
    11.4  
    11.5  (** Isar setup **)
    11.6  
    11.7 -val _ = ML_Context.add_antiq "code" (fn _ => Args.term >> ml_code_antiq);
    11.8 +val _ =
    11.9 +  Context.>> (Context.map_theory
   11.10 +    (ML_Context.add_antiq (Binding.name "code") (fn _ => Args.term >> ml_code_antiq)));
   11.11  
   11.12  local
   11.13  

    12.1 --- a/src/Tools/jEdit/src/isabelle_markup.scala	Mon Jun 27 15:03:55 2011 +0200
    12.2 +++ b/src/Tools/jEdit/src/isabelle_markup.scala	Mon Jun 27 16:53:31 2011 +0200
    12.3 @@ -114,7 +114,8 @@
    12.4      Map(
    12.5        Markup.CLASS -> get_color("red"),
    12.6        Markup.TYPE -> get_color("black"),
    12.7 -      Markup.CONSTANT -> get_color("black"))
    12.8 +      Markup.CONSTANT -> get_color("black"),
    12.9 +      Markup.ML_ANTIQUOTATION -> get_color("black"))
   12.10  
   12.11    private val text_colors: Map[String, Color] =
   12.12      Map(