--- a/src/HOL/Plain.thy Thu Mar 03 15:56:17 2011 +0100 +++ b/src/HOL/Plain.thy Thu Mar 03 18:10:28 2011 +0100 @@ -9,6 +9,4 @@ include @{text Hilbert_Choice}. *} -ML {* Thy_Load.legacy_path_add "~~/src/HOL/Library" *} - end