src/HOL/Tools/datatype_rep_proofs.ML
changeset 18728 6790126ab5f6
parent 18377 0e1d025d57b3
child 19346 c4c003abd830
     1.1 --- a/src/HOL/Tools/datatype_rep_proofs.ML	Fri Jan 20 04:53:59 2006 +0100
     1.2 +++ b/src/HOL/Tools/datatype_rep_proofs.ML	Sat Jan 21 23:02:14 2006 +0100
     1.3 @@ -15,7 +15,7 @@
     1.4  sig
     1.5    val representation_proofs : bool -> DatatypeAux.datatype_info Symtab.table ->
     1.6      string list -> DatatypeAux.descr list -> (string * sort) list ->
     1.7 -      (string * mixfix) list -> (string * mixfix) list list -> theory attribute
     1.8 +      (string * mixfix) list -> (string * mixfix) list list -> attribute
     1.9          -> theory -> (thm list list * thm list list * thm list list *
    1.10            DatatypeAux.simproc_dist list * thm) * theory
    1.11  end;