--- a/src/HOL/Tools/Datatype/datatype_data.ML Mon Jan 10 08:18:49 2011 +0100
+++ b/src/HOL/Tools/Datatype/datatype_data.ML Mon Jan 10 15:19:48 2011 +0100
@@ -71,8 +71,9 @@
let
val tab = Symtab.lookup_list ((#constrs o DatatypesData.get) thy) c;
val hint = case body_type T of Type (tyco, _) => SOME tyco | _ => NONE;
- val default = if null tab then NONE
- else SOME (snd (Library.last_elem tab))
+ val default =
+ if null tab then NONE
+ else SOME (snd (List.last tab))
(*conservative wrt. overloaded constructors*);
in case hint
of NONE => default