# HG changeset patch
# User wenzelm
# Date 1138894294 -3600
# Node ID 2487aea6ff12fc2bb02094d2477a067650161b31
# Parent  5542716503ab189d7ea5b72ed9f3aa0257a9b5c8
always use Attrib.src;

diff -r 5542716503ab -r 2487aea6ff12 src/Pure/Isar/element.ML
--- a/src/Pure/Isar/element.ML	Thu Feb 02 16:31:33 2006 +0100
+++ b/src/Pure/Isar/element.ML	Thu Feb 02 16:31:34 2006 +0100
@@ -33,11 +33,11 @@
   val inst_term: typ Symtab.table * term Symtab.table -> term -> term
   val inst_thm: theory -> typ Symtab.table * term Symtab.table -> thm -> thm
   val inst_ctxt: theory -> typ Symtab.table * term Symtab.table -> context_i -> context_i
-  datatype ('typ, 'term, 'att) stmt =
-    Shows of ((string * 'att list) * ('term * ('term list * 'term list)) list) list |
+  datatype ('typ, 'term) stmt =
+    Shows of ((string * Attrib.src list) * ('term * ('term list * 'term list)) list) list |
     Obtains of (string * ((string * 'typ option) list * 'term list)) list
-  type statement  (*= (string, string, Attrib.src) stmt*)
-  type statement_i  (*= (typ, term, attribute) stmt*)
+  type statement  (*= (string, string) stmt*)
+  type statement_i  (*= (typ, term) stmt*)
 end;
 
 structure Element: ELEMENT =
@@ -261,11 +261,11 @@
 
 (** concluding statements **)
 
-datatype ('typ, 'term, 'att) stmt =
-  Shows of ((string * 'att list) * ('term * ('term list * 'term list)) list) list |
+datatype ('typ, 'term) stmt =
+  Shows of ((string * Attrib.src list) * ('term * ('term list * 'term list)) list) list |
   Obtains of (string * ((string * 'typ option) list * 'term list)) list;
 
-type statement = (string, string, Attrib.src) stmt;
-type statement_i = (typ, term, attribute) stmt;
+type statement = (string, string) stmt;
+type statement_i = (typ, term) stmt;
 
 end;