src/Pure/Isar/auto_bind.ML

     _ $ t => SOME (Term.list_abs (Logic.strip_params prop, t))
   | _ => NONE);
 
 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)];
 
 end;