| changeset 41414 | 00b2b6716ed8 |
| parent 41027 | c599955d9806 |
| child 41430 | 1aa23e9f2c87 |
--- a/src/HOL/HOLCF/HOLCF.thy Wed Dec 29 17:34:41 2010 +0100 +++ b/src/HOL/HOLCF/HOLCF.thy Wed Dec 29 18:18:42 2010 +0100 @@ -13,7 +13,7 @@ default_sort "domain" -ML {* path_add "~~/src/HOL/HOLCF/Library" *} +ML {* Thy_Load.legacy_path_add "~~/src/HOL/HOLCF/Library" *} text {* Legacy theorem names deprecated after Isabelle2009-2: *}