# HG changeset patch
# User wenzelm
# Date 1332188179 -3600
# Node ID c7a89ecbc71e74e9242529365ceb1a67a25174b7
# Parent  8eac39af4ec0cfa1999bbf48ba244dba8daa975a
discontinued remains of duplicate exception UnequalLengths (cf. 441260986b63);

diff -r 8eac39af4ec0 -r c7a89ecbc71e src/Pure/library.ML
--- a/src/Pure/library.ML	Mon Mar 19 21:10:33 2012 +0100
+++ b/src/Pure/library.ML	Mon Mar 19 21:16:19 2012 +0100
@@ -1082,4 +1082,3 @@
 structure Basic_Library: BASIC_LIBRARY = Library;
 open Basic_Library;
 
-datatype legacy = UnequalLengths;