# HG changeset patch
# User blanchet
# Date 1286267450 -7200
# Node ID 186a3b447e0bf0d6253a098406a3d07576321339
# Parent  317010af89727c46729f713370a9913a215f41c9
more explicit name

diff -r 317010af8972 -r 186a3b447e0b src/HOL/Tools/Meson/meson_clausify.ML
--- a/src/HOL/Tools/Meson/meson_clausify.ML	Tue Oct 05 10:28:11 2010 +0200
+++ b/src/HOL/Tools/Meson/meson_clausify.ML	Tue Oct 05 10:30:50 2010 +0200
@@ -213,7 +213,7 @@
     fun tacf [prem] =
       rewrite_goals_tac skolem_def_raw
       THEN rtac ((prem |> rewrite_rule skolem_def_raw)
-                 RS Global_Theory.get_thm thy "someI_ex") 1
+                 RS Global_Theory.get_thm thy "Hilbert_Choice.someI_ex") 1
   in
     Goal.prove_internal [ex_tm] conc tacf
     |> forall_intr_list frees