1.1 --- a/src/Pure/Isar/attrib.ML	Mon Aug 04 20:27:38 2008 +0200
     1.2 +++ b/src/Pure/Isar/attrib.ML	Mon Aug 04 20:27:39 2008 +0200
     1.3 @@ -5,15 +5,10 @@
     1.4  Symbolic representation of attributes -- with name and syntax.
     1.5  *)
     1.6  
     1.7 -signature BASIC_ATTRIB =
     1.8 -sig
     1.9 -  val print_attributes: theory -> unit
    1.10 -end;
    1.11 -
    1.12  signature ATTRIB =
    1.13  sig
    1.14 -  include BASIC_ATTRIB
    1.15 -  type src
    1.16 +  type src = Args.src
    1.17 +  val print_attributes: theory -> unit
    1.18    val intern: theory -> xstring -> string
    1.19    val intern_src: theory -> src -> src
    1.20    val pretty_attribs: Proof.context -> src list -> Pretty.T list
    1.21 @@ -51,6 +46,7 @@
    1.22  
    1.23  type src = Args.src;
    1.24  
    1.25 +
    1.26  (** named attributes **)
    1.27  
    1.28  (* theory data *)
    1.29 @@ -392,6 +388,3 @@
    1.30    register_config MetaSimplifier.simp_depth_limit_value));
    1.31  
    1.32  end;
    1.33 -
    1.34 -structure BasicAttrib: BASIC_ATTRIB = Attrib;
    1.35 -open BasicAttrib;

     2.1 --- a/src/Pure/Isar/method.ML	Mon Aug 04 20:27:38 2008 +0200
     2.2 +++ b/src/Pure/Isar/method.ML	Mon Aug 04 20:27:39 2008 +0200
     2.3 @@ -11,7 +11,6 @@
     2.4    val HEADGOAL: (int -> thm -> 'a Seq.seq) -> thm -> 'a Seq.seq
     2.5    type method
     2.6    val trace_rules: bool ref
     2.7 -  val print_methods: theory -> unit
     2.8  end;
     2.9  
    2.10  signature METHOD =
    2.11 @@ -54,7 +53,7 @@
    2.12    val set_tactic: (thm list -> tactic) -> Proof.context -> Proof.context
    2.13    val tactic: string * Position.T -> Proof.context -> method
    2.14    val raw_tactic: string * Position.T -> Proof.context -> method
    2.15 -  type src
    2.16 +  type src = Args.src
    2.17    datatype text =
    2.18      Basic of (Proof.context -> method) * Position.T |
    2.19      Source of src |
    2.20 @@ -71,6 +70,7 @@
    2.21    val done_text: text
    2.22    val sorry_text: bool -> text
    2.23    val finish_text: text option * bool -> Position.T -> text
    2.24 +  val print_methods: theory -> unit
    2.25    val intern: theory -> xstring -> string
    2.26    val defined: theory -> string -> bool
    2.27    val method: theory -> src -> Proof.context -> method
    2.28 @@ -646,7 +646,6 @@
    2.29  in val parse_args = meth3 end;
    2.30  
    2.31  
    2.32 -
    2.33  (*final declarations of this structure!*)
    2.34  val unfold = unfold_meth;
    2.35  val fold = fold_meth;