src/Pure/Isar/method.ML
changeset 27729 aaf08262b177
parent 27383 cbb4dafea38a
child 27751 22c32eb18c23
     1.1 --- a/src/Pure/Isar/method.ML	Mon Aug 04 20:27:38 2008 +0200
     1.2 +++ b/src/Pure/Isar/method.ML	Mon Aug 04 20:27:39 2008 +0200
     1.3 @@ -11,7 +11,6 @@
     1.4    val HEADGOAL: (int -> thm -> 'a Seq.seq) -> thm -> 'a Seq.seq
     1.5    type method
     1.6    val trace_rules: bool ref
     1.7 -  val print_methods: theory -> unit
     1.8  end;
     1.9  
    1.10  signature METHOD =
    1.11 @@ -54,7 +53,7 @@
    1.12    val set_tactic: (thm list -> tactic) -> Proof.context -> Proof.context
    1.13    val tactic: string * Position.T -> Proof.context -> method
    1.14    val raw_tactic: string * Position.T -> Proof.context -> method
    1.15 -  type src
    1.16 +  type src = Args.src
    1.17    datatype text =
    1.18      Basic of (Proof.context -> method) * Position.T |
    1.19      Source of src |
    1.20 @@ -71,6 +70,7 @@
    1.21    val done_text: text
    1.22    val sorry_text: bool -> text
    1.23    val finish_text: text option * bool -> Position.T -> text
    1.24 +  val print_methods: theory -> unit
    1.25    val intern: theory -> xstring -> string
    1.26    val defined: theory -> string -> bool
    1.27    val method: theory -> src -> Proof.context -> method
    1.28 @@ -646,7 +646,6 @@
    1.29  in val parse_args = meth3 end;
    1.30  
    1.31  
    1.32 -
    1.33  (*final declarations of this structure!*)
    1.34  val unfold = unfold_meth;
    1.35  val fold = fold_meth;