tuned Method exports: non-pervasive type method (cf. Proof.method), pervasive METHOD combinators;

--- a/src/Pure/Isar/method.ML	Fri Mar 13 15:52:23 2009 +0100
+++ b/src/Pure/Isar/method.ML	Fri Mar 13 19:10:46 2009 +0100
@@ -8,13 +8,13 @@
 sig
   val FINDGOAL: (int -> thm -> 'a Seq.seq) -> thm -> 'a Seq.seq
   val HEADGOAL: (int -> thm -> 'a Seq.seq) -> thm -> 'a Seq.seq
-  type method
   val trace_rules: bool ref
 end;
 
 signature METHOD =
 sig
   include BASIC_METHOD
+  type method
   val apply: Position.T -> (Proof.context -> method) -> Proof.context -> thm list -> cases_tactic
   val RAW_METHOD_CASES: (thm list -> cases_tactic) -> method
   val RAW_METHOD: (thm list -> tactic) -> method
@@ -540,3 +540,12 @@
 
 structure BasicMethod: BASIC_METHOD = Method;
 open BasicMethod;
+
+val RAW_METHOD_CASES = Method.RAW_METHOD_CASES;
+val RAW_METHOD = Method.RAW_METHOD;
+val METHOD_CASES = Method.METHOD_CASES;
+val METHOD = Method.METHOD;
+val SIMPLE_METHOD = Method.SIMPLE_METHOD;
+val SIMPLE_METHOD' = Method.SIMPLE_METHOD';
+val SIMPLE_METHOD'' = Method.SIMPLE_METHOD'';
+