1.1 --- a/src/HOL/Hilbert_Choice.thy	Wed Dec 05 03:06:05 2001 +0100
     1.2 +++ b/src/HOL/Hilbert_Choice.thy	Wed Dec 05 03:07:44 2001 +0100
     1.3 @@ -37,6 +37,8 @@
     1.4  
     1.5  
     1.6  use "Hilbert_Choice_lemmas.ML"
     1.7 +declare someI_ex [elim?];
     1.8 +
     1.9  
    1.10  lemma tfl_some: "\<forall>P x. P x --> P (Eps P)"
    1.11    -- {* dynamically-scoped fact for TFL *}