# HG changeset patch
# User wenzelm
# Date 1369994418 -7200
# Node ID 39d60668f8dfa227ff126279b77e26bd26fcd19f
# Parent  2bbeab01c0eae161276f5c9f5727c0bb6b91be12
tuned;

diff -r 2bbeab01c0ea -r 39d60668f8df src/HOL/Spec_Check/spec_check.ML
--- a/src/HOL/Spec_Check/spec_check.ML	Fri May 31 11:56:48 2013 +0200
+++ b/src/HOL/Spec_Check/spec_check.ML	Fri May 31 12:00:18 2013 +0200
@@ -128,11 +128,11 @@
   let
     val return = Unsynchronized.ref "return"
     val use_context : use_context =
-     {tune_source = ML_Parse.fix_ints,
-      name_space = ML_Env.name_space,
-      str_of_pos = Position.here oo Position.line_file,
+     {tune_source = #tune_source ML_Env.local_context,
+      name_space = #name_space ML_Env.local_context,
+      str_of_pos = #str_of_pos ML_Env.local_context,
       print = fn r => return := r,
-      error = error}
+      error = #error ML_Env.local_context}
     val _ =
       Context.setmp_thread_data (SOME (Context.Proof ctxt))
         (fn () => Secure.use_text use_context (0, "generated code") true s) ()