src/HOL/Tools/Datatype/datatype_rep_proofs.ML
changeset 32907 0300f8dd63ea
parent 32904 9d27ebc82700
child 32957 675c0c7e6a37
     1.1 --- a/src/HOL/Tools/Datatype/datatype_rep_proofs.ML	Mon Oct 12 11:03:10 2009 +0200
     1.2 +++ b/src/HOL/Tools/Datatype/datatype_rep_proofs.ML	Mon Oct 12 13:40:28 2009 +0200
     1.3 @@ -15,7 +15,7 @@
     1.4    val representation_proofs : config -> info Symtab.table ->
     1.5      string list -> descr list -> (string * sort) list ->
     1.6        (binding * mixfix) list -> (binding * mixfix) list list -> attribute
     1.7 -        -> theory -> (thm list list * (thm list list * thm list list) * thm) * theory
     1.8 +        -> theory -> (thm list list * thm list list * thm) * theory
     1.9  end;
    1.10  
    1.11  structure DatatypeRepProofs : DATATYPE_REP_PROOFS =
    1.12 @@ -617,7 +617,7 @@
    1.13        ||> Theory.checkpoint;
    1.14  
    1.15    in
    1.16 -    ((constr_inject', (distinct_thms', dist_rewrites), dt_induct'), thy7)
    1.17 +    ((constr_inject', distinct_thms', dt_induct'), thy7)
    1.18    end;
    1.19  
    1.20  end;