src/Pure/Isar/local_defs.ML

--- a/src/Pure/Isar/local_defs.ML	Tue Mar 20 21:37:31 2012 +0100
+++ b/src/Pure/Isar/local_defs.ML	Wed Mar 21 11:00:34 2012 +0100
@@ -173,7 +173,7 @@
 
 val is_trivial = Pattern.aeconv o Logic.dest_equals o Thm.prop_of;
 
-fun trans_list _ _ [] = raise Empty
+fun trans_list _ _ [] = raise List.Empty
   | trans_list trans ctxt (th :: raw_eqs) =
       (case filter_out is_trivial raw_eqs of
         [] => th