src/Pure/Isar/method.ML

   val try_intros_tac: Proof.context -> thm list -> thm list -> tactic
   val rule: Proof.context -> thm list -> method
   val erule: Proof.context -> int -> thm list -> method
   val drule: Proof.context -> int -> thm list -> method
   val frule: Proof.context -> int -> thm list -> method
+  val method_space: Context.generic -> Name_Space.T
   val set_tactic: (morphism -> thm list -> tactic) -> Context.generic -> Context.generic
   val clean_facts: thm list -> thm list
   val set_facts: thm list -> Proof.context -> Proof.context
   val get_facts: Proof.context -> thm list
   type combinator_info

 
 val ops_methods =
  {get_data = get_methods,
   put_data = fn methods => map_data (fn (_, ml_tactic, facts) => (methods, ml_tactic, facts))};
 
+val method_space = Name_Space.space_of_table o get_methods;
+
 
 (* ML tactic *)
 
 fun set_tactic ml_tactic = map_data (fn (methods, _, facts) => (methods, SOME ml_tactic, facts));