--- a/src/HOL/Hilbert_Choice.thy Thu Jun 18 18:31:14 2009 -0700
+++ b/src/HOL/Hilbert_Choice.thy Fri Jun 19 17:23:21 2009 +0200
@@ -7,7 +7,7 @@
theory Hilbert_Choice
imports Nat Wellfounded Plain
-uses ("Tools/meson.ML") ("Tools/specification_package.ML")
+uses ("Tools/meson.ML") ("Tools/choice_specification.ML")
begin
subsection {* Hilbert's epsilon *}
@@ -596,7 +596,7 @@
lemma exE_some: "[| Ex P ; c == Eps P |] ==> P c"
by (simp only: someI_ex)
-use "Tools/specification_package.ML"
+use "Tools/choice_specification.ML"
end