always use Attrib.src;
authorwenzelm
Thu Feb 02 16:31:34 2006 +0100 (2006-02-02)
changeset 189062487aea6ff12
parent 18905 5542716503ab
child 18907 f984f22f1cb4
always use Attrib.src;
src/Pure/Isar/element.ML
     1.1 --- a/src/Pure/Isar/element.ML	Thu Feb 02 16:31:33 2006 +0100
     1.2 +++ b/src/Pure/Isar/element.ML	Thu Feb 02 16:31:34 2006 +0100
     1.3 @@ -33,11 +33,11 @@
     1.4    val inst_term: typ Symtab.table * term Symtab.table -> term -> term
     1.5    val inst_thm: theory -> typ Symtab.table * term Symtab.table -> thm -> thm
     1.6    val inst_ctxt: theory -> typ Symtab.table * term Symtab.table -> context_i -> context_i
     1.7 -  datatype ('typ, 'term, 'att) stmt =
     1.8 -    Shows of ((string * 'att list) * ('term * ('term list * 'term list)) list) list |
     1.9 +  datatype ('typ, 'term) stmt =
    1.10 +    Shows of ((string * Attrib.src list) * ('term * ('term list * 'term list)) list) list |
    1.11      Obtains of (string * ((string * 'typ option) list * 'term list)) list
    1.12 -  type statement  (*= (string, string, Attrib.src) stmt*)
    1.13 -  type statement_i  (*= (typ, term, attribute) stmt*)
    1.14 +  type statement  (*= (string, string) stmt*)
    1.15 +  type statement_i  (*= (typ, term) stmt*)
    1.16  end;
    1.17  
    1.18  structure Element: ELEMENT =
    1.19 @@ -261,11 +261,11 @@
    1.20  
    1.21  (** concluding statements **)
    1.22  
    1.23 -datatype ('typ, 'term, 'att) stmt =
    1.24 -  Shows of ((string * 'att list) * ('term * ('term list * 'term list)) list) list |
    1.25 +datatype ('typ, 'term) stmt =
    1.26 +  Shows of ((string * Attrib.src list) * ('term * ('term list * 'term list)) list) list |
    1.27    Obtains of (string * ((string * 'typ option) list * 'term list)) list;
    1.28  
    1.29 -type statement = (string, string, Attrib.src) stmt;
    1.30 -type statement_i = (typ, term, attribute) stmt;
    1.31 +type statement = (string, string) stmt;
    1.32 +type statement_i = (typ, term) stmt;
    1.33  
    1.34  end;