# HG changeset patch
# User wenzelm
# Date 968172709 -7200
# Node ID b4a170f7d658ac5c89ea39f9ef164b80874b54c3
# Parent  67cdb658e4226f1c90d9a5e5a26fbe0813f36a7f
generalized types of args;

diff -r 67cdb658e422 -r b4a170f7d658 src/Pure/Isar/method.ML
--- a/src/Pure/Isar/method.ML	Tue Sep 05 18:51:25 2000 +0200
+++ b/src/Pure/Isar/method.ML	Tue Sep 05 18:51:49 2000 +0200
@@ -71,21 +71,20 @@
   type modifier
   val sectioned_args: (Proof.context * Args.T list -> 'a * (Proof.context * Args.T list)) ->
     (Args.T list -> modifier * Args.T list) list ->
-    ('a -> Proof.context -> Proof.method) -> Args.src -> Proof.context -> Proof.method
+    ('a -> Proof.context -> 'b) -> Args.src -> Proof.context -> 'b
   val bang_sectioned_args:
     (Args.T list -> modifier * Args.T list) list ->
-    (thm list -> Proof.context -> Proof.method) -> Args.src -> Proof.context -> Proof.method
+    (thm list -> Proof.context -> 'a) -> Args.src -> Proof.context -> 'a
   val bang_sectioned_args':
     (Args.T list -> modifier * Args.T list) list ->
     (Proof.context * Args.T list -> 'a * (Proof.context * Args.T list)) ->
-    ('a -> thm list -> Proof.context -> Proof.method) -> Args.src -> Proof.context -> Proof.method
+    ('a -> thm list -> Proof.context -> 'b) -> Args.src -> Proof.context -> 'b
   val only_sectioned_args:
     (Args.T list -> modifier * Args.T list) list ->
-    (Proof.context -> Proof.method) -> Args.src -> Proof.context -> Proof.method
-  val thms_ctxt_args: (thm list -> Proof.context -> Proof.method)
-    -> Args.src -> Proof.context -> Proof.method
-  val thms_args: (thm list -> Proof.method) -> Args.src -> Proof.context -> Proof.method
-  val thm_args: (thm -> Proof.method) -> Args.src -> Proof.context -> Proof.method
+    (Proof.context -> 'a) -> Args.src -> Proof.context -> 'a
+  val thms_ctxt_args: (thm list -> Proof.context -> 'a) -> Args.src -> Proof.context -> 'a
+  val thms_args: (thm list -> 'a) -> Args.src -> Proof.context -> 'a
+  val thm_args: (thm -> 'a) -> Args.src -> Proof.context -> 'a
   datatype text =
     Basic of (Proof.context -> Proof.method) |
     Source of Args.src |