# HG changeset patch # User wenzelm # Date 1394309290 -3600 # Node ID 9dc5ce83202cde2e2a1807e43bb0253117016207 # Parent 13a7d9661ffc24a74930949ae1fb7838036f3fa5 modernized Attrib.check_name/check_src similar to methods (see also a989bdaf8121); proper context for global data; tuned signature; diff -r 13a7d9661ffc -r 9dc5ce83202c src/Doc/antiquote_setup.ML --- 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" #> diff -r 13a7d9661ffc -r 9dc5ce83202c src/HOL/Library/simps_case_conv.ML --- 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 diff -r 13a7d9661ffc -r 9dc5ce83202c src/HOL/Tools/Function/fun_cases.ML --- 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"} diff -r 13a7d9661ffc -r 9dc5ce83202c src/HOL/Tools/inductive.ML --- 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; diff -r 13a7d9661ffc -r 9dc5ce83202c src/HOL/Tools/recdef.ML --- 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); diff -r 13a7d9661ffc -r 9dc5ce83202c src/HOL/Tools/try0.ML --- 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; diff -r 13a7d9661ffc -r 9dc5ce83202c src/Pure/Isar/args.ML --- 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, []); diff -r 13a7d9661ffc -r 9dc5ce83202c src/Pure/Isar/attrib.ML --- 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; diff -r 13a7d9661ffc -r 9dc5ce83202c src/Pure/Isar/bundle.ML --- 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; diff -r 13a7d9661ffc -r 9dc5ce83202c src/Pure/Isar/element.ML --- 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; diff -r 13a7d9661ffc -r 9dc5ce83202c src/Pure/Isar/expression.ML --- 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 *) diff -r 13a7d9661ffc -r 9dc5ce83202c src/Pure/Isar/isar_syn.ML --- 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"} diff -r 13a7d9661ffc -r 9dc5ce83202c src/Pure/Isar/method.ML --- 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 *) diff -r 13a7d9661ffc -r 9dc5ce83202c src/Pure/Isar/proof.ML --- 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) diff -r 13a7d9661ffc -r 9dc5ce83202c src/Pure/Isar/specification.ML --- 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 ())); diff -r 13a7d9661ffc -r 9dc5ce83202c src/Pure/ML/ml_thms.ML --- 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); diff -r 13a7d9661ffc -r 9dc5ce83202c src/Tools/permanent_interpretation.ML --- 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 *)