modernized Attrib.check_name/check_src similar to methods (see also a989bdaf8121);
proper context for global data;
tuned signature;

--- a/src/Doc/antiquote_setup.ML	Sat Mar 08 13:49:01 2014 +0100
+++ b/src/Doc/antiquote_setup.ML	Sat Mar 08 21:08:10 2014 +0100
@@ -230,7 +230,7 @@
   entity_antiqs (K (Keyword.is_keyword o #1)) "isakeyword" "keyword" #>
   entity_antiqs (K (Keyword.is_keyword o #1)) "isakeyword" "element" #>
   entity_antiqs (can o Method.check_name) "" "method" #>
-  entity_antiqs (can o Attrib.check o Proof_Context.theory_of) "" "attribute" #>
+  entity_antiqs (can o Attrib.check_name) "" "attribute" #>
   entity_antiqs no_check "" "fact" #>
   entity_antiqs no_check "" "variable" #>
   entity_antiqs no_check "" "case" #>

--- a/src/HOL/Library/simps_case_conv.ML	Sat Mar 08 13:49:01 2014 +0100
+++ b/src/HOL/Library/simps_case_conv.ML	Sat Mar 08 21:08:10 2014 +0100
@@ -202,8 +202,7 @@
 
 fun case_of_simps_cmd (bind, thms_ref) lthy =
   let
-    val thy = Proof_Context.theory_of lthy
-    val bind' = apsnd (map (Attrib.intern_src thy)) bind
+    val bind' = apsnd (map (Attrib.check_src lthy)) bind
     val thm = (Attrib.eval_thms lthy) thms_ref |> to_case lthy
   in
     Local_Theory.note (bind', [thm]) lthy |> snd
@@ -211,8 +210,7 @@
 
 fun simps_of_case_cmd ((bind, thm_ref), splits_ref) lthy =
   let
-    val thy = Proof_Context.theory_of lthy
-    val bind' = apsnd (map (Attrib.intern_src thy)) bind
+    val bind' = apsnd (map (Attrib.check_src lthy)) bind
     val thm = singleton (Attrib.eval_thms lthy) thm_ref
     val simps = if null splits_ref
       then to_simps lthy thm

--- a/src/HOL/Tools/Function/fun_cases.ML	Sat Mar 08 13:49:01 2014 +0100
+++ b/src/HOL/Tools/Function/fun_cases.ML	Sat Mar 08 21:08:10 2014 +0100
@@ -43,17 +43,16 @@
 
 fun gen_fun_cases prep_att prep_prop args lthy =
   let
-    val thy = Proof_Context.theory_of lthy;
     val thmss =
       map snd args
       |> burrow (grouped 10 Par_List.map (mk_fun_cases lthy o prep_prop lthy));
     val facts =
-      map2 (fn ((a, atts), _) => fn thms => ((a, map (prep_att thy) atts), [(thms, [])]))
+      map2 (fn ((a, atts), _) => fn thms => ((a, map (prep_att lthy) atts), [(thms, [])]))
         args thmss;
   in lthy |> Local_Theory.notes facts end;
 
 val fun_cases = gen_fun_cases (K I) Syntax.check_prop;
-val fun_cases_cmd = gen_fun_cases Attrib.intern_src Syntax.read_prop;
+val fun_cases_cmd = gen_fun_cases Attrib.check_src Syntax.read_prop;
 
 val _ =
   Outer_Syntax.local_theory @{command_spec "fun_cases"}

--- a/src/HOL/Tools/inductive.ML	Sat Mar 08 13:49:01 2014 +0100
+++ b/src/HOL/Tools/inductive.ML	Sat Mar 08 21:08:10 2014 +0100
@@ -576,16 +576,15 @@
 
 fun gen_inductive_cases prep_att prep_prop args lthy =
   let
-    val thy = Proof_Context.theory_of lthy;
     val thmss =
       map snd args
       |> burrow (grouped 10 Par_List.map (mk_cases lthy o prep_prop lthy));
     val facts =
-      map2 (fn ((a, atts), _) => fn thms => ((a, map (prep_att thy) atts), [(thms, [])]))
+      map2 (fn ((a, atts), _) => fn thms => ((a, map (prep_att lthy) atts), [(thms, [])]))
         args thmss;
   in lthy |> Local_Theory.notes facts end;
 
-val inductive_cases = gen_inductive_cases Attrib.intern_src Syntax.read_prop;
+val inductive_cases = gen_inductive_cases Attrib.check_src Syntax.read_prop;
 val inductive_cases_i = gen_inductive_cases (K I) Syntax.check_prop;
 
 
@@ -635,13 +634,12 @@
 
 fun gen_inductive_simps prep_att prep_prop args lthy =
   let
-    val thy = Proof_Context.theory_of lthy;
     val facts = args |> map (fn ((a, atts), props) =>
-      ((a, map (prep_att thy) atts),
+      ((a, map (prep_att lthy) atts),
         map (Thm.no_attributes o single o mk_simp_eq lthy o prep_prop lthy) props));
   in lthy |> Local_Theory.notes facts end;
 
-val inductive_simps = gen_inductive_simps Attrib.intern_src Syntax.read_prop;
+val inductive_simps = gen_inductive_simps Attrib.check_src Syntax.read_prop;
 val inductive_simps_i = gen_inductive_simps (K I) Syntax.check_prop;
 
 

--- a/src/HOL/Tools/recdef.ML	Sat Mar 08 13:49:01 2014 +0100
+++ b/src/HOL/Tools/recdef.ML	Sat Mar 08 21:08:10 2014 +0100
@@ -253,7 +253,7 @@
   let
     val thy = Proof_Context.theory_of lthy;
     val name = prep_name thy raw_name;
-    val atts = map (prep_att thy) raw_atts;
+    val atts = map (prep_att lthy) raw_atts;
     val tcs =
       (case get_recdef thy name of
         NONE => error ("No recdef definition of constant: " ^ quote name)
@@ -268,7 +268,7 @@
       (Element.Shows [(Attrib.empty_binding, [(HOLogic.mk_Trueprop tc, [])])]) int lthy
   end;
 
-val recdef_tc = gen_recdef_tc Attrib.intern_src Sign.intern_const;
+val recdef_tc = gen_recdef_tc Attrib.check_src Sign.intern_const;
 val recdef_tc_i = gen_recdef_tc (K I) (K I);
 
 

--- a/src/HOL/Tools/try0.ML	Sat Mar 08 13:49:01 2014 +0100
+++ b/src/HOL/Tools/try0.ML	Sat Mar 08 21:08:10 2014 +0100
@@ -57,8 +57,7 @@
 
 fun apply_named_method_on_first_goal ctxt =
   parse_method
-  #> Method.check_source ctxt
-  #> Method.the_method ctxt
+  #> Method.method_cmd ctxt
   #> Method.Basic
   #> (fn m => Method.Select_Goals (Method.no_combinator_info, 1, m))
   #> Proof.refine;

--- a/src/Pure/Isar/args.ML	Sat Mar 08 13:49:01 2014 +0100
+++ b/src/Pure/Isar/args.ML	Sat Mar 08 21:08:10 2014 +0100
@@ -61,10 +61,10 @@
   val goal_spec: ((int -> tactic) -> tactic) context_parser
   val parse: Token.T list parser
   val parse1: (string -> bool) -> Token.T list parser
-  val attribs: (string -> string) -> src list parser
-  val opt_attribs: (string -> string) -> src list parser
-  val thm_name: (string -> string) -> string -> (binding * src list) parser
-  val opt_thm_name: (string -> string) -> string -> (binding * src list) parser
+  val attribs: (xstring * Position.T -> string) -> src list parser
+  val opt_attribs: (xstring * Position.T -> string) -> src list parser
+  val thm_name: (xstring * Position.T -> string) -> string -> (binding * src list) parser
+  val opt_thm_name: (xstring * Position.T -> string) -> string -> (binding * src list) parser
   val syntax: string -> 'a context_parser -> src -> Context.generic -> 'a * Context.generic
   val context_syntax: string -> 'a context_parser -> src -> Proof.context -> 'a * Proof.context
 end;
@@ -261,23 +261,23 @@
 
 (* attributes *)
 
-fun attribs intern =
+fun attribs check =
   let
-    val attrib_name = internal_text || (symbolic || named)
-      >> evaluate Token.Text (intern o Token.content_of);
+    fun intern tok = check (Token.content_of tok, Token.pos_of tok);
+    val attrib_name = internal_text || (symbolic || named) >> evaluate Token.Text intern;
     val attrib = Parse.position (attrib_name -- Parse.!!! parse) >> src;
   in $$$ "[" |-- Parse.!!! (Parse.list attrib --| $$$ "]") end;
 
-fun opt_attribs intern = Scan.optional (attribs intern) [];
+fun opt_attribs check = Scan.optional (attribs check) [];
 
 
 (* theorem specifications *)
 
-fun thm_name intern s = binding -- opt_attribs intern --| $$$ s;
+fun thm_name check_attrib s = binding -- opt_attribs check_attrib --| $$$ s;
 
-fun opt_thm_name intern s =
+fun opt_thm_name check_attrib s =
   Scan.optional
-    ((binding -- opt_attribs intern || attribs intern >> pair Binding.empty) --| $$$ s)
+    ((binding -- opt_attribs check_attrib || attribs check_attrib >> pair Binding.empty) --| $$$ s)
     (Binding.empty, []);
 
 

--- a/src/Pure/Isar/attrib.ML	Sat Mar 08 13:49:01 2014 +0100
+++ b/src/Pure/Isar/attrib.ML	Sat Mar 08 21:08:10 2014 +0100
@@ -10,10 +10,11 @@
   type binding = binding * src list
   val empty_binding: binding
   val is_empty_binding: binding -> bool
-  val print_attributes: theory -> unit
-  val check: theory -> xstring * Position.T -> string
-  val intern: theory -> xstring -> string
-  val intern_src: theory -> src -> src
+  val print_attributes: Proof.context -> unit
+  val check_name_generic: Context.generic -> xstring * Position.T -> string
+  val check_src_generic: Context.generic -> src -> src
+  val check_name: Proof.context -> xstring * Position.T -> string
+  val check_src: Proof.context -> src -> src
   val pretty_attribs: Proof.context -> src list -> Pretty.T list
   val attribute: Proof.context -> src -> attribute
   val attribute_global: theory -> src -> attribute
@@ -94,10 +95,11 @@
   fun merge data : T = Name_Space.merge_tables data;
 );
 
-fun print_attributes thy =
+val get_attributes = Attributes.get o Context.theory_of;
+
+fun print_attributes ctxt =
   let
-    val ctxt = Proof_Context.init_global thy;
-    val attribs = Attributes.get thy;
+    val attribs = get_attributes (Context.Proof ctxt);
     fun prt_attr (name, (_, "")) = Pretty.mark_str name
       | prt_attr (name, (_, comment)) =
           Pretty.block
@@ -111,18 +113,24 @@
   |> Attributes.map (Name_Space.define (Context.Theory thy) true (name, (att, comment)) #> snd);
 
 
-(* name space *)
+(* check *)
 
-fun check thy = #1 o Name_Space.check (Context.Theory thy) (Attributes.get thy);
+fun check_name_generic context = #1 o Name_Space.check context (get_attributes context);
 
-val intern = Name_Space.intern o #1 o Attributes.get;
-val intern_src = Args.map_name o intern;
+fun check_src_generic context src =
+  let
+    val ((xname, toks), pos) = Args.dest_src src;
+    val name = check_name_generic context (xname, pos);
+  in Args.src ((name, toks), pos) end;
 
-fun extern ctxt = Name_Space.extern ctxt (#1 (Attributes.get (Proof_Context.theory_of ctxt)));
+val check_name = check_name_generic o Context.Proof;
+val check_src = check_src_generic o Context.Proof;
 
 
 (* pretty printing *)
 
+fun extern ctxt = Name_Space.extern ctxt (#1 (get_attributes (Context.Proof ctxt)));
+
 fun pretty_attribs _ [] = []
   | pretty_attribs ctxt srcs =
       [Pretty.enum "," "[" "]" (map (Args.pretty_src ctxt o Args.map_name (extern ctxt)) srcs)];
@@ -131,23 +139,20 @@
 (* get attributes *)
 
 fun attribute_generic context =
-  let
-    val thy = Context.theory_of context;
-    val (space, tab) = Attributes.get thy;
-    fun attr src =
+  let val (_, tab) = get_attributes context in
+    fn src =>
       let val ((name, _), pos) = Args.dest_src src in
         (case Symtab.lookup tab name of
-          NONE => error ("Unknown attribute: " ^ quote name ^ Position.here pos)
-        | SOME (att, _) =>
-            (Context_Position.report_generic context pos (Name_Space.markup space name); att src))
-      end;
-  in attr end;
+          NONE => error ("Undefined attribute: " ^ quote name ^ Position.here pos)
+        | SOME (att, _) => att src)
+      end
+  end;
 
 val attribute = attribute_generic o Context.Proof;
 val attribute_global = attribute_generic o Context.Theory;
 
-fun attribute_cmd ctxt = attribute ctxt o intern_src (Proof_Context.theory_of ctxt);
-fun attribute_cmd_global thy = attribute_global thy o intern_src thy;
+fun attribute_cmd ctxt = attribute ctxt o check_src ctxt;
+fun attribute_cmd_global thy = attribute_global thy o check_src_generic (Context.Theory thy);
 
 
 (* attributed declarations *)
@@ -221,12 +226,11 @@
 
 fun gen_thm pick = Scan.depend (fn context =>
   let
-    val thy = Context.theory_of context;
     val get = Context.cases (Global_Theory.get_fact context) Proof_Context.get_fact context;
     val get_fact = get o Facts.Fact;
     fun get_named pos name = get (Facts.Named ((name, pos), NONE));
   in
-    Parse.$$$ "[" |-- Args.attribs (intern thy) --| Parse.$$$ "]" >> (fn srcs =>
+    Parse.$$$ "[" |-- Args.attribs (check_name_generic context) --| Parse.$$$ "]" >> (fn srcs =>
       let
         val atts = map (attribute_generic context) srcs;
         val (th', context') = fold (uncurry o Thm.apply_attribute) atts (Drule.dummy_thm, context);
@@ -237,7 +241,7 @@
      Scan.ahead (Parse.position fact_name) :|-- (fn (name, pos) =>
       Args.named_fact (get_named pos) -- Scan.option thm_sel
         >> (fn (fact, sel) => (name, Facts.Named ((name, pos), sel), fact))))
-    -- Args.opt_attribs (intern thy) >> (fn ((name, thmref, fact), srcs) =>
+    -- Args.opt_attribs (check_name_generic context) >> (fn ((name, thmref, fact), srcs) =>
       let
         val ths = Facts.select thmref fact;
         val atts = map (attribute_generic context) srcs;
@@ -340,13 +344,13 @@
 
 fun print_options ctxt =
   let
-    val thy = Proof_Context.theory_of ctxt;
     fun prt (name, config) =
       let val value = Config.get ctxt config in
         Pretty.block [Pretty.mark_str name, Pretty.str (": " ^ Config.print_type value ^ " ="),
           Pretty.brk 1, Pretty.str (Config.print_value value)]
       end;
-    val configs = Name_Space.extern_table ctxt (#1 (Attributes.get thy), Configs.get thy);
+    val space = #1 (get_attributes (Context.Proof ctxt));
+    val configs = Name_Space.extern_table ctxt (space, Configs.get (Proof_Context.theory_of ctxt));
   in Pretty.writeln (Pretty.big_list "configuration options" (map prt configs)) end;
 
 

--- a/src/Pure/Isar/bundle.ML	Sat Mar 08 13:49:01 2014 +0100
+++ b/src/Pure/Isar/bundle.ML	Sat Mar 08 21:08:10 2014 +0100
@@ -76,9 +76,7 @@
 in
 
 val bundle = gen_bundle (K I) (K I) Proof_Context.cert_vars;
-val bundle_cmd =
-  gen_bundle Proof_Context.get_fact (Attrib.intern_src o Proof_Context.theory_of)
-    Proof_Context.read_vars;
+val bundle_cmd = gen_bundle Proof_Context.get_fact Attrib.check_src Proof_Context.read_vars;
 
 end;
 

--- a/src/Pure/Isar/element.ML	Sat Mar 08 13:49:01 2014 +0100
+++ b/src/Pure/Isar/element.ML	Sat Mar 08 21:08:10 2014 +0100
@@ -528,7 +528,7 @@
     term = I,
     pattern = I,
     fact = Proof_Context.get_fact ctxt,
-    attrib = Attrib.intern_src (Proof_Context.theory_of ctxt)}
+    attrib = Attrib.check_src ctxt}
   in activate_i elem ctxt end;
 
 end;

--- a/src/Pure/Isar/expression.ML	Sat Mar 08 13:49:01 2014 +0100
+++ b/src/Pure/Isar/expression.ML	Sat Mar 08 21:08:10 2014 +0100
@@ -851,8 +851,7 @@
   let
     val ((propss, deps, export), expr_ctxt) = prep_expr expression initial_ctxt;
     val eqns = prep_with_extended_syntax prep_prop deps expr_ctxt raw_eqns;
-    val attrss =
-      map (apsnd (map (prep_attr (Proof_Context.theory_of initial_ctxt))) o fst) raw_eqns;
+    val attrss = map (apsnd (map (prep_attr initial_ctxt)) o fst) raw_eqns;
     val goal_ctxt = fold Variable.auto_fixes eqns expr_ctxt;
     val export' = Variable.export_morphism goal_ctxt expr_ctxt;
   in (((propss, deps, export, export'), (eqns, attrss)), goal_ctxt) end;
@@ -861,7 +860,7 @@
   prep_interpretation cert_goal_expression (K I) (K I);
 
 val read_interpretation =
-  prep_interpretation read_goal_expression Syntax.parse_prop Attrib.intern_src;
+  prep_interpretation read_goal_expression Syntax.parse_prop Attrib.check_src;
 
 
 (* generic interpretation machinery *)

--- a/src/Pure/Isar/isar_syn.ML	Sat Mar 08 13:49:01 2014 +0100
+++ b/src/Pure/Isar/isar_syn.ML	Sat Mar 08 21:08:10 2014 +0100
@@ -799,7 +799,7 @@
   Outer_Syntax.improper_command @{command_spec "print_attributes"}
     "print attributes of this theory"
     (Scan.succeed (Toplevel.unknown_theory o
-      Toplevel.keep (Attrib.print_attributes o Toplevel.theory_of)));
+      Toplevel.keep (Attrib.print_attributes o Toplevel.context_of)));
 
 val _ =
   Outer_Syntax.improper_command @{command_spec "print_simpset"}

--- a/src/Pure/Isar/method.ML	Sat Mar 08 13:49:01 2014 +0100
+++ b/src/Pure/Isar/method.ML	Sat Mar 08 21:08:10 2014 +0100
@@ -63,9 +63,10 @@
   val sorry_text: bool -> text
   val finish_text: text option * bool -> text
   val print_methods: Proof.context -> unit
-  val the_method: Proof.context -> src -> Proof.context -> method
   val check_name: Proof.context -> xstring * Position.T -> string
-  val check_source: Proof.context -> src -> src
+  val check_src: Proof.context -> src -> src
+  val method: Proof.context -> src -> Proof.context -> method
+  val method_cmd: Proof.context -> src -> Proof.context -> method
   val syntax: 'a context_parser -> src -> Proof.context -> 'a * Proof.context
   val setup: binding -> (Proof.context -> method) context_parser -> string -> theory -> theory
   val method_setup: bstring * Position.T -> Symbol_Pos.source -> string -> theory -> theory
@@ -335,26 +336,31 @@
 fun add_method name meth comment thy = thy
   |> Methods.map (Name_Space.define (Context.Theory thy) true (name, (meth, comment)) #> snd);
 
-fun the_method ctxt =
+
+(* check *)
+
+fun check_name ctxt = #1 o Name_Space.check (Context.Proof ctxt) (get_methods ctxt);
+
+fun check_src ctxt src =
+  let
+    val ((xname, toks), pos) = Args.dest_src src;
+    val name = check_name ctxt (xname, pos);
+  in Args.src ((name, toks), pos) end;
+
+
+(* get methods *)
+
+fun method ctxt =
   let val (_, tab) = get_methods ctxt in
     fn src =>
       let val ((name, _), pos) = Args.dest_src src in
         (case Symtab.lookup tab name of
           NONE => error ("Undefined method: " ^ quote name ^ Position.here pos)
-        | SOME (method, _) => method src)
+        | SOME (meth, _) => meth src)
       end
   end;
 
-
-(* check *)
-
-fun check_name ctxt = #1 o Name_Space.check (Context.Proof ctxt) (get_methods ctxt);
-
-fun check_source ctxt src =
-  let
-    val ((xname, toks), pos) = Args.dest_src src;
-    val name = check_name ctxt (xname, pos);
-  in Args.src ((name, toks), pos) end;
+fun method_cmd ctxt = method ctxt o check_src ctxt;
 
 
 (* method setup *)

--- a/src/Pure/Isar/proof.ML	Sat Mar 08 13:49:01 2014 +0100
+++ b/src/Pure/Isar/proof.ML	Sat Mar 08 21:08:10 2014 +0100
@@ -421,8 +421,7 @@
     val ctxt = context_of state;
 
     fun eval (Method.Basic m) = apply_method current_context m
-      | eval (Method.Source src) =
-          apply_method current_context (Method.the_method ctxt (Method.check_source ctxt src))
+      | eval (Method.Source src) = apply_method current_context (Method.method_cmd ctxt src)
       | eval (Method.Then (_, txts)) = Seq.EVERY (map eval txts)
       | eval (Method.Orelse (_, txts)) = Seq.FIRST (map eval txts)
       | eval (Method.Try (_, txt)) = Seq.TRY (eval txt)

--- a/src/Pure/Isar/specification.ML	Sat Mar 08 13:49:01 2014 +0100
+++ b/src/Pure/Isar/specification.ML	Sat Mar 08 21:08:10 2014 +0100
@@ -113,8 +113,6 @@
 
 fun prepare prep_vars parse_prop prep_att do_close raw_vars raw_specss ctxt =
   let
-    val thy = Proof_Context.theory_of ctxt;
-
     val (vars, vars_ctxt) = ctxt |> prep_vars raw_vars;
     val (xs, params_ctxt) = vars_ctxt |> Proof_Context.add_fixes vars;
 
@@ -136,7 +134,7 @@
 
     val Ts = specs_ctxt |> fold_map Proof_Context.inferred_param xs |> fst;
     val params = map2 (fn (b, _, mx) => fn T => ((b, T), mx)) vars Ts;
-    val name_atts = map (fn ((name, atts), _) => (name, map (prep_att thy) atts)) (flat raw_specss);
+    val name_atts = map (fn ((name, atts), _) => (name, map (prep_att ctxt) atts)) (flat raw_specss);
   in ((params, name_atts ~~ specs), specs_ctxt) end;
 
 
@@ -150,16 +148,16 @@
 in
 
 fun check_spec x = prep_spec Proof_Context.cert_vars (K I) (K I) true x;
-fun read_spec x = prep_spec Proof_Context.read_vars Syntax.parse_prop Attrib.intern_src true x;
+fun read_spec x = prep_spec Proof_Context.read_vars Syntax.parse_prop Attrib.check_src true x;
 
 fun check_free_spec x = prep_spec Proof_Context.cert_vars (K I) (K I) false x;
-fun read_free_spec x = prep_spec Proof_Context.read_vars Syntax.parse_prop Attrib.intern_src false x;
+fun read_free_spec x = prep_spec Proof_Context.read_vars Syntax.parse_prop Attrib.check_src false x;
 
 fun check_specification vars specs =
   prepare Proof_Context.cert_vars (K I) (K I) true vars [specs];
 
 fun read_specification vars specs =
-  prepare Proof_Context.read_vars Syntax.parse_prop Attrib.intern_src true vars [specs];
+  prepare Proof_Context.read_vars Syntax.parse_prop Attrib.check_src true vars [specs];
 
 end;
 
@@ -293,10 +291,9 @@
 fun gen_theorems prep_fact prep_att prep_vars
     kind raw_facts raw_fixes int lthy =
   let
-    val attrib = prep_att (Proof_Context.theory_of lthy);
     val facts = raw_facts |> map (fn ((name, atts), bs) =>
-      ((name, map attrib atts),
-        bs |> map (fn (b, more_atts) => (prep_fact lthy b, map attrib more_atts))));
+      ((name, map (prep_att lthy) atts),
+        bs |> map (fn (b, more_atts) => (prep_fact lthy b, map (prep_att lthy) more_atts))));
     val (_, ctxt') = lthy |> prep_vars raw_fixes |-> Proof_Context.add_fixes;
 
     val facts' = facts
@@ -309,7 +306,7 @@
 in
 
 val theorems = gen_theorems (K I) (K I) Proof_Context.cert_vars;
-val theorems_cmd = gen_theorems Proof_Context.get_fact Attrib.intern_src Proof_Context.read_vars;
+val theorems_cmd = gen_theorems Proof_Context.get_fact Attrib.check_src Proof_Context.read_vars;
 
 end;
 
@@ -384,15 +381,12 @@
     kind before_qed after_qed (name, raw_atts) raw_includes raw_elems raw_concl int lthy =
   let
     val _ = Local_Theory.assert lthy;
-    val thy = Proof_Context.theory_of lthy;
 
-    val attrib = prep_att thy;
-
-    val elems = raw_elems |> map (Element.map_ctxt_attrib attrib);
+    val elems = raw_elems |> map (Element.map_ctxt_attrib (prep_att lthy));
     val ((more_atts, prems, stmt, facts), goal_ctxt) = lthy
       |> Bundle.includes (map (prep_bundle lthy) raw_includes)
-      |> prep_statement attrib prep_stmt elems raw_concl;
-    val atts = more_atts @ map attrib raw_atts;
+      |> prep_statement (prep_att lthy) prep_stmt elems raw_concl;
+    val atts = more_atts @ map (prep_att lthy) raw_atts;
 
     fun after_qed' results goal_ctxt' =
       let
@@ -428,11 +422,11 @@
 
 val theorem = gen_theorem false (K I) (K I) Expression.cert_statement;
 val theorem_cmd =
-  gen_theorem false Bundle.check Attrib.intern_src Expression.read_statement;
+  gen_theorem false Bundle.check Attrib.check_src Expression.read_statement;
 
 val schematic_theorem = gen_theorem true (K I) (K I) Expression.cert_statement;
 val schematic_theorem_cmd =
-  gen_theorem true Bundle.check Attrib.intern_src Expression.read_statement;
+  gen_theorem true Bundle.check Attrib.check_src Expression.read_statement;
 
 fun add_theorem_hook f = Theorem_Hook.map (cons (f, stamp ()));
 

--- a/src/Pure/ML/ml_thms.ML	Sat Mar 08 13:49:01 2014 +0100
+++ b/src/Pure/ML/ml_thms.ML	Sat Mar 08 21:08:10 2014 +0100
@@ -39,10 +39,9 @@
     (Scan.depend (fn context => Parse_Spec.attribs >> (fn raw_srcs =>
       let
         val ctxt = Context.the_proof context;
-        val thy = Proof_Context.theory_of ctxt;
 
         val i = serial ();
-        val srcs = map (Attrib.intern_src thy) raw_srcs;
+        val srcs = map (Attrib.check_src ctxt) raw_srcs;
         val _ = map (Attrib.attribute ctxt) srcs;
         val (a, ctxt') = ctxt
           |> ML_Antiquote.variant "attributes" ||> put_attributes (i, srcs);

--- a/src/Tools/permanent_interpretation.ML	Sat Mar 08 13:49:01 2014 +0100
+++ b/src/Tools/permanent_interpretation.ML	Sat Mar 08 21:08:10 2014 +0100
@@ -41,13 +41,16 @@
     (*setting up*)
     val ((propss, deps, export), expr_ctxt) = prep_expr expression base_ctxt;
       (*FIXME: only re-prepare if defs are given*)
-    val attrss = map (apsnd (map (prep_attr (Proof_Context.theory_of expr_ctxt))) o fst) raw_eqns;
+    val attrss = map (apsnd (map (prep_attr expr_ctxt)) o fst) raw_eqns;
     val goal_ctxt = fold Variable.auto_fixes eqns expr_ctxt;
     val export' = Variable.export_morphism goal_ctxt expr_ctxt;
   in (((propss, deps, export, export'), (def_eqns, eqns, attrss)), goal_ctxt) end;
 
-val cert_interpretation = prep_interpretation Expression.cert_goal_expression (K I) (K I) (K I);
-val read_interpretation = prep_interpretation Expression.read_goal_expression Syntax.parse_term Syntax.parse_prop Attrib.intern_src;
+val cert_interpretation =
+  prep_interpretation Expression.cert_goal_expression (K I) (K I) (K I);
+
+val read_interpretation =
+  prep_interpretation Expression.read_goal_expression Syntax.parse_term Syntax.parse_prop Attrib.check_src;
 
 
 (* generic interpretation machinery *)