src/Pure/Isar/proof.ML

   val defer: int option -> state -> state Seq.seq
   val prefer: int -> state -> state Seq.seq
   val apply: Method.text -> state -> state Seq.seq
   val apply_end: Method.text -> state -> state Seq.seq
   val local_goal: (context -> ((string * string) * (string * thm list) list) -> unit) ->
-    (theory -> 'a -> attribute) ->
+    (Proof.context -> 'a -> attribute) ->
     ('b list -> context -> (term list list * (context -> context)) * context) ->
     string -> Method.text option -> (thm list list -> state -> state) ->
     ((binding * 'a list) * 'b) list -> state -> state
   val local_qed: Method.text option * bool -> state -> state
   val theorem: Method.text option -> (thm list list -> context -> context) ->

 fun goals st = map goalN (1 upto Thm.nprems_of st);
 
 fun no_goal_cases st = map (rpair NONE) (goals st);
 
 fun goal_cases st =
-  Rule_Cases.make_common (Thm.theory_of_thm st, Thm.prop_of st) (map (rpair [] o rpair []) (goals st));
+  Rule_Cases.make_common
+    (Thm.theory_of_thm st, Thm.prop_of st) (map (rpair [] o rpair []) (goals st));
 
 fun apply_method current_context meth state =
   let
     val (goal_ctxt, (_, {statement, messages = _, using, goal, before_qed, after_qed})) =
       find_goal state;

 local
 
 fun gen_assume asm prep_att exp args state =
   state
   |> assert_forward
-  |> map_context_result (asm exp (Attrib.map_specs (map (prep_att (theory_of state))) args))
+  |> map_context_result (asm exp (Attrib.map_specs (map (prep_att (context_of state))) args))
   |> these_factss [] |> #2;
 
 in
 
 val assm = gen_assume Proof_Context.add_assms_i (K I);
-val assm_cmd = gen_assume Proof_Context.add_assms Attrib.attribute;
+val assm_cmd = gen_assume Proof_Context.add_assms Attrib.attribute_cmd;
 val assume = assm Assumption.assume_export;
 val assume_cmd = assm_cmd Assumption.assume_export;
 val presume = assm Assumption.presume_export;
 val presume_cmd = assm_cmd Assumption.presume_export;
 

 local
 
 fun gen_def prep_att prep_vars prep_binds args state =
   let
     val _ = assert_forward state;
-    val thy = theory_of state;
-
     val (raw_name_atts, (raw_vars, raw_rhss)) = args |> split_list ||> split_list;
-    val name_atts = map (apsnd (map (prep_att thy))) raw_name_atts;
+    val name_atts = map (apsnd (map (prep_att (context_of state)))) raw_name_atts;
   in
     state
     |> map_context_result (prep_vars (map (fn (x, mx) => (x, NONE, mx)) raw_vars))
     |>> map (fn (x, _, mx) => (x, mx))
     |-> (fn vars =>

   end;
 
 in
 
 val def = gen_def (K I) Proof_Context.cert_vars Proof_Context.match_bind_i;
-val def_cmd = gen_def Attrib.attribute Proof_Context.read_vars Proof_Context.match_bind;
+val def_cmd = gen_def Attrib.attribute_cmd Proof_Context.read_vars Proof_Context.match_bind;
 
 end;
 
 
 

 local
 
 fun gen_thmss more_facts opt_chain opt_result prep_atts prep_fact args state =
   state
   |> assert_forward
-  |> map_context_result (Proof_Context.note_thmss ""
-    (Attrib.map_facts_refs
-      (map (prep_atts (theory_of state)))
-      (prep_fact (context_of state)) args))
+  |> map_context_result (fn ctxt => ctxt |> Proof_Context.note_thmss ""
+    (Attrib.map_facts_refs (map (prep_atts ctxt)) (prep_fact ctxt) args))
   |> these_factss (more_facts state)
   ||> opt_chain
   |> opt_result;
 
 in
 
 val note_thmss = gen_thmss (K []) I #2 (K I) (K I);
-val note_thmss_cmd = gen_thmss (K []) I #2 Attrib.attribute Proof_Context.get_fact;
+val note_thmss_cmd = gen_thmss (K []) I #2 Attrib.attribute_cmd Proof_Context.get_fact;
 
 val from_thmss = gen_thmss (K []) chain #2 (K I) (K I) o no_binding;
-val from_thmss_cmd = gen_thmss (K []) chain #2 Attrib.attribute Proof_Context.get_fact o no_binding;
+val from_thmss_cmd =
+  gen_thmss (K []) chain #2 Attrib.attribute_cmd Proof_Context.get_fact o no_binding;
 
 val with_thmss = gen_thmss the_facts chain #2 (K I) (K I) o no_binding;
-val with_thmss_cmd = gen_thmss the_facts chain #2 Attrib.attribute Proof_Context.get_fact o no_binding;
+val with_thmss_cmd =
+  gen_thmss the_facts chain #2 Attrib.attribute_cmd Proof_Context.get_fact o no_binding;
 
 val local_results = gen_thmss (K []) I I (K I) (K I) o map (apsnd Thm.simple_fact);
 
 end;
 

 
 fun gen_using f g prep_att prep_fact args state =
   state
   |> assert_backward
   |> map_context_result
-    (Proof_Context.note_thmss ""
-      (Attrib.map_facts_refs (map (prep_att (theory_of state))) (prep_fact (context_of state))
-        (no_binding args)))
+    (fn ctxt => ctxt |> Proof_Context.note_thmss ""
+      (Attrib.map_facts_refs (map (prep_att ctxt)) (prep_fact ctxt) (no_binding args)))
   |> (fn (named_facts, state') =>
     state' |> map_goal I (fn (statement, _, using, goal, before_qed, after_qed) =>
       let
         val ctxt = context_of state';
         val ths = maps snd named_facts;

 val unfold_goals = Local_Defs.unfold_goals;
 
 in
 
 val using = gen_using append_using (K (K I)) (K I) (K I);
-val using_cmd = gen_using append_using (K (K I)) Attrib.attribute Proof_Context.get_fact;
+val using_cmd = gen_using append_using (K (K I)) Attrib.attribute_cmd Proof_Context.get_fact;
 val unfolding = gen_using unfold_using unfold_goals (K I) (K I);
-val unfolding_cmd = gen_using unfold_using unfold_goals Attrib.attribute Proof_Context.get_fact;
+val unfolding_cmd = gen_using unfold_using unfold_goals Attrib.attribute_cmd Proof_Context.get_fact;
 
 end;
 
 
 (* case *)

 fun qualified_binding a =
   Binding.qualify true (Long_Name.qualifier a) (Binding.name (Long_Name.base_name a));
 
 fun gen_invoke_case prep_att (name, xs, raw_atts) state =
   let
-    val atts = map (prep_att (theory_of state)) raw_atts;
+    val atts = map (prep_att (context_of state)) raw_atts;
     val (asms, state') = state |> map_context_result (fn ctxt =>
       ctxt |> Proof_Context.apply_case (Proof_Context.get_case ctxt name xs));
     val assumptions = asms |> map (fn (a, ts) => ((qualified_binding a, atts), map (rpair []) ts));
   in
     state'

   end;
 
 in
 
 val invoke_case = gen_invoke_case (K I);
-val invoke_case_cmd = gen_invoke_case Attrib.attribute;
+val invoke_case_cmd = gen_invoke_case Attrib.attribute_cmd;
 
 end;
 
 
 

 
 (* local goals *)
 
 fun local_goal print_results prep_att prepp kind before_qed after_qed stmt state =
   let
-    val thy = theory_of state;
     val ((names, attss), propp) =
-      Attrib.map_specs (map (prep_att thy)) stmt |> split_list |>> split_list;
+      Attrib.map_specs (map (prep_att (context_of state))) stmt |> split_list |>> split_list;
 
     fun after_qed' results =
       local_results ((names ~~ attss) ~~ results)
       #-> (fn res => tap (fn st => print_results (context_of st) ((kind, ""), res) : unit))
       #> after_qed results;

   end;
 
 in
 
 val have = gen_have (K I) Proof_Context.bind_propp_i;
-val have_cmd = gen_have Attrib.attribute Proof_Context.bind_propp;
+val have_cmd = gen_have Attrib.attribute_cmd Proof_Context.bind_propp;
 val show = gen_show (K I) Proof_Context.bind_propp_i;
-val show_cmd = gen_show Attrib.attribute Proof_Context.bind_propp;
+val show_cmd = gen_show Attrib.attribute_cmd Proof_Context.bind_propp;
 
 end;