src/HOL/Tools/old_primrec.ML

--- a/src/HOL/Tools/old_primrec.ML	Mon Sep 28 09:47:32 2009 +0200
+++ b/src/HOL/Tools/old_primrec.ML	Mon Sep 28 10:20:21 2009 +0200
@@ -230,7 +230,7 @@
               (tname, dt)::(find_dts dt_info tnames' tnames)
             else find_dts dt_info tnames' tnames);
 
-fun prepare_induct ({descr, inducts = (_, induct), ...}: info) rec_eqns =
+fun prepare_induct ({descr, induct, ...}: info) rec_eqns =
   let
     fun constrs_of (_, (_, _, cs)) =
       map (fn (cname:string, (_, cargs, _, _, _)) => (cname, map fst cargs)) cs;