# HG changeset patch
# User wenzelm
# Date 1217874459 -7200
# Node ID aaf08262b177b46ad8c6b46befc887c5dbde32ef
# Parent  9a9e54042800b398721ab36d0c16fbcb8d91b9da
tuned signature;
eliminated obsolete pervasives;

diff -r 9a9e54042800 -r aaf08262b177 src/Pure/Isar/attrib.ML
--- a/src/Pure/Isar/attrib.ML	Mon Aug 04 20:27:38 2008 +0200
+++ b/src/Pure/Isar/attrib.ML	Mon Aug 04 20:27:39 2008 +0200
@@ -5,15 +5,10 @@
 Symbolic representation of attributes -- with name and syntax.
 *)
 
-signature BASIC_ATTRIB =
-sig
-  val print_attributes: theory -> unit
-end;
-
 signature ATTRIB =
 sig
-  include BASIC_ATTRIB
-  type src
+  type src = Args.src
+  val print_attributes: theory -> unit
   val intern: theory -> xstring -> string
   val intern_src: theory -> src -> src
   val pretty_attribs: Proof.context -> src list -> Pretty.T list
@@ -51,6 +46,7 @@
 
 type src = Args.src;
 
+
 (** named attributes **)
 
 (* theory data *)
@@ -392,6 +388,3 @@
   register_config MetaSimplifier.simp_depth_limit_value));
 
 end;
-
-structure BasicAttrib: BASIC_ATTRIB = Attrib;
-open BasicAttrib;
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;