# HG changeset patch
# User wenzelm
# Date 1283793061 -7200
# Node ID e6b96b4cde7e41f2a851d3bd2a22924732aa90b9
# Parent  b98909faaea82bb4a3f2280f3f50bb014692ea79
ML_Context.thm;

diff -r b98909faaea8 -r e6b96b4cde7e src/HOL/Tools/TFL/tfl.ML
--- a/src/HOL/Tools/TFL/tfl.ML	Mon Sep 06 14:18:16 2010 +0200
+++ b/src/HOL/Tools/TFL/tfl.ML	Mon Sep 06 19:11:01 2010 +0200
@@ -564,7 +564,7 @@
      val body_th = R.LIST_CONJ (map R.ASSUME full_rqt_prop)
      val SELECT_AX = (*in this way we hope to avoid a STATIC dependence upon
                        theory Hilbert_Choice*)
-         thm "Hilbert_Choice.tfl_some"
+         ML_Context.thm "Hilbert_Choice.tfl_some"
          handle ERROR msg => cat_error msg
     "defer_recdef requires theory Main or at least Hilbert_Choice as parent"
      val bar = R.MP (R.ISPECL[tych R'abs, tych R1] SELECT_AX) body_th