# HG changeset patch
# User haftmann
# Date 1464269270 -7200
# Node ID 534f16b0ca3975831ea1d652d6a3e603dd2e4a74
# Parent  65a81a4ef7f84738cebeb1e53393bf7c0fff38b7
explicit quasi-global context for nbe conversions -- works around quasi-global type variable handling in lift_triv_classes_conv

diff -r 65a81a4ef7f8 -r 534f16b0ca39 src/Tools/nbe.ML
--- a/src/Tools/nbe.ML	Thu May 26 15:27:50 2016 +0200
+++ b/src/Tools/nbe.ML	Thu May 26 15:27:50 2016 +0200
@@ -82,9 +82,11 @@
 
 in
 
-fun lift_triv_classes_conv ctxt conv ct =
+fun lift_triv_classes_conv orig_ctxt conv ct =
   let
-    val thy = Proof_Context.theory_of ctxt;
+    val thy = Proof_Context.theory_of orig_ctxt;
+    val ctxt = Proof_Context.init_global thy;
+      (*FIXME quasi-global context*)
     val algebra = Sign.classes_of thy;
     val triv_classes = get_triv_classes thy;
     fun additional_classes sort = filter_out (fn class => Sorts.sort_le algebra (sort, [class])) triv_classes;
@@ -120,7 +122,7 @@
     |> (map_types o map_type_tfree)
         (fn (v, _) => TFree (v, (fst o the o AList.lookup (op =) vs_tab) v))
     |> Thm.cterm_of ctxt
-    |> conv
+    |> conv ctxt
     |> Thm.strip_shyps
     |> Thm.varifyT_global
     |> Thm.unconstrainT
@@ -597,8 +599,8 @@
   raw_oracle (nbe_program_idx_tab, ctxt, vs_ty_t, deps, ct);
 
 fun dynamic_conv ctxt = lift_triv_classes_conv ctxt
-  (Code_Thingol.dynamic_conv ctxt (fn program =>
-    oracle (compile false ctxt program) ctxt));
+  (fn ctxt' => Code_Thingol.dynamic_conv ctxt' (fn program =>
+    oracle (compile false ctxt program) ctxt'));
 
 fun dynamic_value ctxt = lift_triv_classes_rew ctxt
   (Code_Thingol.dynamic_value ctxt I (fn program =>
@@ -608,7 +610,7 @@
   let
     val conv = Code_Thingol.static_conv_thingol ctxt_consts
       (fn { program, ... } => oracle (compile true ctxt program));
-  in fn ctxt' => lift_triv_classes_conv ctxt' (conv ctxt') end;
+  in fn ctxt' => lift_triv_classes_conv ctxt' conv end;
 
 fun static_value { ctxt, consts } =
   let