src/HOL/Tools/Datatype/datatype_rep_proofs.ML
changeset 32727 9072201cd69d
parent 32712 ec5976f4d3d8
child 32765 3032c0308019
     1.1 --- a/src/HOL/Tools/Datatype/datatype_rep_proofs.ML	Mon Sep 28 09:47:32 2009 +0200
     1.2 +++ b/src/HOL/Tools/Datatype/datatype_rep_proofs.ML	Mon Sep 28 10:20:21 2009 +0200
     1.3 @@ -389,7 +389,7 @@
     1.4      fun prove_iso_thms (ds, (inj_thms, elem_thms)) =
     1.5        let
     1.6          val (_, (tname, _, _)) = hd ds;
     1.7 -        val induct = (snd o #inducts o the o Symtab.lookup dt_info) tname;
     1.8 +        val induct = (#induct o the o Symtab.lookup dt_info) tname;
     1.9  
    1.10          fun mk_ind_concl (i, _) =
    1.11            let