diff -r 2df6ad1dbd66 -r 2a526bd279ed src/HOL/Cardinals/Wellorder_Extension.thy --- a/src/HOL/Cardinals/Wellorder_Extension.thy Thu Jan 16 16:20:17 2014 +0100 +++ b/src/HOL/Cardinals/Wellorder_Extension.thy Thu Jan 16 16:33:19 2014 +0100 @@ -5,7 +5,7 @@ header {* Extending Well-founded Relations to Wellorders *} theory Wellorder_Extension -imports "~~/src/HOL/Library/Zorn" Order_Union +imports Zorn Order_Union begin subsection {* Extending Well-founded Relations to Wellorders *}