diff -r 9a9e54042800 -r aaf08262b177 src/Pure/Isar/method.ML
--- a/src/Pure/Isar/method.ML	Mon Aug 04 20:27:38 2008 +0200
+++ b/src/Pure/Isar/method.ML	Mon Aug 04 20:27:39 2008 +0200
@@ -11,7 +11,6 @@
   val HEADGOAL: (int -> thm -> 'a Seq.seq) -> thm -> 'a Seq.seq
   type method
   val trace_rules: bool ref
-  val print_methods: theory -> unit
 end;
 
 signature METHOD =
@@ -54,7 +53,7 @@
   val set_tactic: (thm list -> tactic) -> Proof.context -> Proof.context
   val tactic: string * Position.T -> Proof.context -> method
   val raw_tactic: string * Position.T -> Proof.context -> method
-  type src
+  type src = Args.src
   datatype text =
     Basic of (Proof.context -> method) * Position.T |
     Source of src |
@@ -71,6 +70,7 @@
   val done_text: text
   val sorry_text: bool -> text
   val finish_text: text option * bool -> Position.T -> text
+  val print_methods: theory -> unit
   val intern: theory -> xstring -> string
   val defined: theory -> string -> bool
   val method: theory -> src -> Proof.context -> method
@@ -646,7 +646,6 @@
 in val parse_args = meth3 end;
 
 
-
 (*final declarations of this structure!*)
 val unfold = unfold_meth;
 val fold = fold_meth;