--- 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;
--- 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;