src/Pure/Isar/auto_bind.ML

--- a/src/Pure/Isar/auto_bind.ML	Mon Jan 10 08:18:49 2011 +0100
+++ b/src/Pure/Isar/auto_bind.ML	Mon Jan 10 15:19:48 2011 +0100
@@ -44,7 +44,7 @@
 
 fun facts _ [] = []
   | facts thy props =
-      let val prop = Library.last_elem props
+      let val prop = List.last props
       in [(Syntax.dddot_indexname, get_arg thy prop)] @ statement_binds thy thisN prop end;
 
 val no_facts = [(Syntax.dddot_indexname, NONE), ((thisN, 0), NONE)];