--- a/src/Pure/Isar/method.ML Tue Sep 07 20:27:06 2021 +0200
+++ b/src/Pure/Isar/method.ML Tue Sep 07 21:16:22 2021 +0200
@@ -38,6 +38,7 @@
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
@@ -312,6 +313,8 @@
{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 *)