src/HOL/Tools/Meson/meson_clausify.ML
changeset 39949 186a3b447e0b
parent 39948 317010af8972
child 39950 f3c4849868b8
     1.1 --- a/src/HOL/Tools/Meson/meson_clausify.ML	Tue Oct 05 10:28:11 2010 +0200
     1.2 +++ b/src/HOL/Tools/Meson/meson_clausify.ML	Tue Oct 05 10:30:50 2010 +0200
     1.3 @@ -213,7 +213,7 @@
     1.4      fun tacf [prem] =
     1.5        rewrite_goals_tac skolem_def_raw
     1.6        THEN rtac ((prem |> rewrite_rule skolem_def_raw)
     1.7 -                 RS Global_Theory.get_thm thy "someI_ex") 1
     1.8 +                 RS Global_Theory.get_thm thy "Hilbert_Choice.someI_ex") 1
     1.9    in
    1.10      Goal.prove_internal [ex_tm] conc tacf
    1.11      |> forall_intr_list frees