ML_Context.thm;
authorwenzelm
Mon Sep 06 19:11:01 2010 +0200 (2010-09-06)
changeset 39158e6b96b4cde7e
parent 39157 b98909faaea8
child 39159 0dec18004e75
ML_Context.thm;
src/HOL/Tools/TFL/tfl.ML
     1.1 --- a/src/HOL/Tools/TFL/tfl.ML	Mon Sep 06 14:18:16 2010 +0200
     1.2 +++ b/src/HOL/Tools/TFL/tfl.ML	Mon Sep 06 19:11:01 2010 +0200
     1.3 @@ -564,7 +564,7 @@
     1.4       val body_th = R.LIST_CONJ (map R.ASSUME full_rqt_prop)
     1.5       val SELECT_AX = (*in this way we hope to avoid a STATIC dependence upon
     1.6                         theory Hilbert_Choice*)
     1.7 -         thm "Hilbert_Choice.tfl_some"
     1.8 +         ML_Context.thm "Hilbert_Choice.tfl_some"
     1.9           handle ERROR msg => cat_error msg
    1.10      "defer_recdef requires theory Main or at least Hilbert_Choice as parent"
    1.11       val bar = R.MP (R.ISPECL[tych R'abs, tych R1] SELECT_AX) body_th