# HG changeset patch
# User wenzelm
# Date 962310689 -7200
# Node ID a57987e0250b50771ac25a958204d067b6a43e9b
# Parent  4f4936582889cc6c808bccf4ebdbda03fe08a9b6
added add_method;

diff -r 4f4936582889 -r a57987e0250b src/Pure/Isar/method.ML
--- a/src/Pure/Isar/method.ML	Thu Jun 29 22:31:12 2000 +0200
+++ b/src/Pure/Isar/method.ML	Thu Jun 29 22:31:29 2000 +0200
@@ -55,6 +55,7 @@
   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
     -> theory -> theory
   val syntax: (Proof.context * Args.T list -> 'a * (Proof.context * Args.T list)) ->
@@ -417,7 +418,7 @@
   in meth end;
 
 
-(* add_methods *)
+(* add_method(s) *)
 
 fun add_methods raw_meths thy =
   let
@@ -433,6 +434,8 @@
     thy |> MethodsData.put {space = space', meths = meths'}
   end;
 
+val add_method = add_methods o Library.single;
+
 (*implicit version*)
 fun Method name meth cmt = Context.>> (add_methods [(name, meth, cmt)]);