# HG changeset patch
# User wenzelm
# Date 962473523 -7200
# Node ID 92ad2341179dbf4dd09a28e70f8bfa28e8bc923b
# Parent  e1fd1003d5f9db86aa6a7e879d995a6f00f16b03
removed help_methods;
tuned print_methods;

diff -r e1fd1003d5f9 -r 92ad2341179d src/Pure/Isar/method.ML
--- a/src/Pure/Isar/method.ML	Sat Jul 01 19:44:57 2000 +0200
+++ b/src/Pure/Isar/method.ML	Sat Jul 01 19:45:23 2000 +0200
@@ -53,7 +53,6 @@
   val set_tactic: (Proof.context -> thm list -> tactic) -> unit
   val tactic: string -> Proof.context -> Proof.method
   exception METHOD_FAIL of (string * Position.T) * exn
-  val help_methods: theory option -> Pretty.T list
   val method: theory -> Args.src -> Proof.context -> Proof.method
   val add_method: bstring * (Args.src -> Proof.context -> Proof.method) * string -> theory -> theory
   val add_methods: (bstring * (Args.src -> Proof.context -> Proof.method) * string) list
@@ -379,24 +378,19 @@
       meths = Symtab.merge eq_snd (meths1, meths2) handle Symtab.DUPS dups =>
         error ("Attempt to merge different versions of methods " ^ commas_quote dups)};
 
-  fun pretty_meths verbose {space, meths} =
+  fun print _ {space, meths} =
     let
       fun prt_meth (name, ((_, comment), _)) = Pretty.block
         [Pretty.str (name ^ ":"), Pretty.brk 2, Pretty.str comment];
     in
-      (if not verbose then [] else [Display.pretty_name_space ("method name space", space)]) @
       [Pretty.big_list "methods:" (map prt_meth (NameSpace.cond_extern_table space meths))]
+      |> Pretty.chunks |> Pretty.writeln
     end;
-
-  fun print _ = Pretty.writeln o Pretty.chunks o pretty_meths true;
 end;
 
 structure MethodsData = TheoryDataFun(MethodsDataArgs);
 val print_methods = MethodsData.print;
 
-fun help_methods None = [Pretty.str "methods: (unkown theory context)"]
-  | help_methods (Some thy) = MethodsDataArgs.pretty_meths false (MethodsData.get thy);
-
 
 (* get methods *)