src/HOL/Tools/meson.ML

--- a/src/HOL/Tools/meson.ML	Fri Apr 30 23:43:09 2010 +0200
+++ b/src/HOL/Tools/meson.ML	Fri Apr 30 23:53:37 2010 +0200
@@ -555,7 +555,7 @@
         skolemize_nnf_list ctxt ths);
 
 fun add_clauses th cls =
-  let val ctxt0 = Variable.thm_context th
+  let val ctxt0 = Variable.global_thm_context th
       val (cnfs, ctxt) = make_cnf [] th ctxt0
   in Variable.export ctxt ctxt0 cnfs @ cls end;