help: unkown theory context;

--- a/src/Pure/Isar/attrib.ML	Sun Sep 26 16:38:50 1999 +0200
+++ b/src/Pure/Isar/attrib.ML	Sun Sep 26 16:39:54 1999 +0200
@@ -15,7 +15,7 @@
 signature ATTRIB =
 sig
   include BASIC_ATTRIB
-  val help_attributes: theory -> unit
+  val help_attributes: theory option -> unit
   exception ATTRIB_FAIL of (string * Position.T) * exn
   val global_attribute: theory -> Args.src -> theory attribute
   val local_attribute: theory -> Args.src -> Proof.context attribute
@@ -75,7 +75,9 @@
 
 structure AttributesData = TheoryDataFun(AttributesDataArgs);
 val print_attributes = AttributesData.print;
-val help_attributes = AttributesDataArgs.print_atts false o AttributesData.get;
+
+fun help_attributes None = writeln "attributes: (unkown theory context)"
+  | help_attributes (Some thy) = AttributesDataArgs.print_atts false (AttributesData.get thy);
 
 
 (* get global / local attributes *)

--- a/src/Pure/Isar/method.ML	Sun Sep 26 16:38:50 1999 +0200
+++ b/src/Pure/Isar/method.ML	Sun Sep 26 16:39:54 1999 +0200
@@ -31,7 +31,7 @@
   val erule: thm list -> Proof.method
   val assumption: Proof.context -> Proof.method
   exception METHOD_FAIL of (string * Position.T) * exn
-  val help_methods: theory -> unit
+  val help_methods: theory option -> unit
   val method: theory -> Args.src -> Proof.context -> Proof.method
   val add_methods: (bstring * (Args.src -> Proof.context -> Proof.method) * string) list
     -> theory -> theory
@@ -212,7 +212,9 @@
 
 structure MethodsData = TheoryDataFun(MethodsDataArgs);
 val print_methods = MethodsData.print;
-val help_methods = MethodsDataArgs.print_meths false o MethodsData.get;
+
+fun help_methods None = writeln "methods: (unkown theory context)"
+  | help_methods (Some thy) = MethodsDataArgs.print_meths false (MethodsData.get thy);
 
 
 (* get methods *)