diff -r 5e8a0b8bb070 -r 52fd62618631 src/HOL/BNF/Tools/bnf_def.ML
--- a/src/HOL/BNF/Tools/bnf_def.ML	Sat May 11 16:13:08 2013 +0200
+++ b/src/HOL/BNF/Tools/bnf_def.ML	Sat May 11 16:57:18 2013 +0200
@@ -123,7 +123,7 @@
   {map_id = id, map_comp = comp, map_cong0 = cong, set_map = nat, bd_card_order = c_o,
    bd_cinfinite = cinf, set_bd = set_bd, in_bd = in_bd, map_wpull = wpull, rel_OO_Grp = rel};
 
-fun dest_cons [] = raise Empty
+fun dest_cons [] = raise List.Empty
   | dest_cons (x :: xs) = (x, xs);
 
 fun mk_axioms n thms = thms