# HG changeset patch
# User haftmann
# Date 1262610613 -3600
# Node ID 54621a41b03c8a48d0ca00341e586315ad276fa0
# Parent  b28be884eddad46c816d1484e537422ab4a70ff8# Parent  6fb7dd3fd81adfeb31bee3624214351694bc86c8
merged

diff -r b28be884edda -r 54621a41b03c src/Pure/Isar/code.ML
--- a/src/Pure/Isar/code.ML	Mon Jan 04 11:55:23 2010 +0100
+++ b/src/Pure/Isar/code.ML	Mon Jan 04 14:10:13 2010 +0100
@@ -76,8 +76,8 @@
 signature CODE_DATA =
 sig
   type T
-  val change: theory -> (T -> T) -> T
-  val change_yield: theory -> (T -> 'a * T) -> 'a * T
+  val change: theory -> (theory -> T -> T) -> T
+  val change_yield: theory -> (theory -> T -> 'a * T) -> 'a * T
 end;
 
 signature PRIVATE_CODE =
@@ -85,9 +85,9 @@
   include CODE
   val declare_data: Object.T -> serial
   val change_data: serial * ('a -> Object.T) * (Object.T -> 'a)
-    -> theory -> ('a -> 'a) -> 'a
+    -> theory -> (theory -> 'a -> 'a) -> 'a
   val change_yield_data: serial * ('a -> Object.T) * (Object.T -> 'a)
-    -> theory -> ('a -> 'b * 'a) -> 'b * 'a
+    -> theory -> (theory -> 'a -> 'b * 'a) -> 'b * 'a
 end;
 
 structure Code : PRIVATE_CODE =
@@ -234,53 +234,35 @@
 local
 
 type data = Object.T Datatab.table;
-fun create_data data = Synchronized.var "code data" data;
-fun empty_data () = create_data Datatab.empty : data Synchronized.var;
+fun empty_dataref () = Synchronized.var "code data" (NONE : (data * theory_ref) option);
 
-structure Code_Data = TheoryDataFun
+structure Code_Data = Theory_Data
 (
-  type T = spec * data Synchronized.var;
+  type T = spec * (data * theory_ref) option Synchronized.var;
   val empty = (make_spec (false, (((Symtab.empty, Symtab.empty), Symtab.empty),
-    (Symtab.empty, (Symtab.empty, Symtab.empty)))), empty_data ());
-  fun copy (spec, data) = (spec, create_data (Synchronized.value data));
-  val extend = copy;
-  fun merge _ ((spec1, _), (spec2, _)) =
-    (merge_spec (spec1, spec2), empty_data ());
+    (Symtab.empty, (Symtab.empty, Symtab.empty)))), empty_dataref ());
+  val extend = I
+  fun merge ((spec1, _), (spec2, _)) =
+    (merge_spec (spec1, spec2), empty_dataref ());
 );
 
-fun thy_data f thy = f ((snd o Code_Data.get) thy);
-
-fun get_ensure_init kind data =
-  case Datatab.lookup (Synchronized.value data) kind
-   of SOME x => x
-    | NONE => let val y = invoke_init kind
-        in (Synchronized.change data (Datatab.update (kind, y)); y) end;
-
 in
 
 (* access to executable code *)
 
 val the_exec = fst o Code_Data.get;
 
-fun map_exec_purge f =
-  Code_Data.map (fn (exec, data) => (f exec, empty_data ()));
+fun map_exec_purge f = Code_Data.map (fn (exec, _) => (f exec, empty_dataref ()));
 
-val purge_data = (Code_Data.map o apsnd) (fn _ => empty_data ());
+val purge_data = (Code_Data.map o apsnd) (fn _ => empty_dataref ());
 
 fun change_eqns delete c f = (map_exec_purge o map_eqns
   o (if delete then Symtab.map_entry c else Symtab.map_default (c, ((false, (true, [])), [])))
     o apfst) (fn (_, eqns) => (true, f eqns));
 
-fun del_eqns c = change_eqns true c (K (false, []));
-
 
 (* tackling equation history *)
 
-fun get_eqns thy c =
-  Symtab.lookup ((the_eqns o the_exec) thy) c
-  |> Option.map (snd o snd o fst)
-  |> these;
-
 fun continue_history thy = if (history_concluded o the_exec) thy
   then thy
     |> (Code_Data.map o apfst o map_history_concluded) (K false)
@@ -297,30 +279,26 @@
         #> map_history_concluded (K true))
     |> SOME;
 
-val _ = Context.>> (Context.map_theory (Code_Data.init
-  #> Theory.at_begin continue_history
-  #> Theory.at_end conclude_history));
+val _ = Context.>> (Context.map_theory (Theory.at_begin continue_history #> Theory.at_end conclude_history));
 
 
 (* access to data dependent on abstract executable code *)
 
-fun change_data (kind, mk, dest) =
+fun change_yield_data (kind, mk, dest) theory f =
   let
-    fun chnge data_ref f =
-      let
-        val data = get_ensure_init kind data_ref;
-        val data' = f (dest data);
-      in (Synchronized.change data_ref (Datatab.update (kind, mk data')); data') end;
-  in thy_data chnge end;
+    val dataref = (snd o Code_Data.get) theory;
+    val (datatab, thy, thy_ref) = case Synchronized.value dataref
+     of SOME (datatab, thy_ref) => (datatab, Theory.deref thy_ref, thy_ref)
+      | NONE => (Datatab.empty, theory, Theory.check_thy theory)
+    val data = case Datatab.lookup datatab kind
+     of SOME data => data
+      | NONE => invoke_init kind;
+    val result as (x, data') = f thy (dest data);
+    val _ = Synchronized.change dataref
+      ((K o SOME) (Datatab.update (kind, mk data') datatab, thy_ref));
+  in result end;
 
-fun change_yield_data (kind, mk, dest) =
-  let
-    fun chnge data_ref f =
-      let
-        val data = get_ensure_init kind data_ref;
-        val (x, data') = f (dest data);
-      in (x, (Synchronized.change data_ref (Datatab.update (kind, mk data')); data')) end;
-  in thy_data chnge end;
+fun change_data ops theory f = change_yield_data ops theory (pair () oo f) |> snd;
 
 end; (*local*)
 
@@ -574,7 +552,9 @@
   in map2 (fn vs => Thm.certify_instantiate (vs ~~ vts, [])) vss thms end;
 
 fun these_eqns thy c =
-  get_eqns thy c
+  Symtab.lookup ((the_eqns o the_exec) thy) c
+  |> Option.map (snd o snd o fst)
+  |> these
   |> (map o apfst) (Thm.transfer thy)
   |> burrow_fst (standard_typscheme thy);
 
@@ -709,38 +689,6 @@
 val add_signature_cmd = gen_add_signature read_const read_signature;
 
 
-(* datatypes *)
-
-structure Type_Interpretation =
-  Interpretation(type T = string * serial val eq = eq_snd (op =) : T * T -> bool);
-
-fun add_datatype raw_cs thy =
-  let
-    val cs = map (fn c_ty as (_, ty) => (AxClass.unoverload_const thy c_ty, ty)) raw_cs;
-    val (tyco, vs_cos) = constrset_of_consts thy cs;
-    val old_cs = (map fst o snd o get_datatype thy) tyco;
-    fun drop_outdated_cases cases = fold Symtab.delete_safe
-      (Symtab.fold (fn (c, (_, (_, cos))) =>
-        if exists (member (op =) old_cs) cos
-          then insert (op =) c else I) cases []) cases;
-  in
-    thy
-    |> fold (del_eqns o fst) cs
-    |> map_exec_purge
-        ((map_dtyps o Symtab.map_default (tyco, [])) (cons (serial (), vs_cos))
-        #> (map_cases o apfst) drop_outdated_cases)
-    |> Type_Interpretation.data (tyco, serial ())
-  end;
-
-fun type_interpretation f =  Type_Interpretation.interpretation
-  (fn (tyco, _) => fn thy => f (tyco, get_datatype thy tyco) thy);
-
-fun add_datatype_cmd raw_cs thy =
-  let
-    val cs = map (read_bare_const thy) raw_cs;
-  in add_datatype cs thy end;
-
-
 (* code equations *)
 
 fun gen_add_eqn default (thm, proper) thy =
@@ -773,6 +721,56 @@
  of SOME (thm, _) => change_eqns true (const_eqn thy thm) (del_thm thm) thy
   | NONE => thy;
 
+fun del_eqns c = change_eqns true c (K (false, []));
+
+
+(* cases *)
+
+fun add_case thm thy =
+  let
+    val (c, (k, case_pats)) = case_cert thm;
+    val _ = case filter_out (is_constr thy) case_pats
+     of [] => ()
+      | cs => error ("Non-constructor(s) in case certificate: " ^ commas (map quote cs));
+    val entry = (1 + Int.max (1, length case_pats), (k, case_pats))
+  in (map_exec_purge o map_cases o apfst) (Symtab.update (c, entry)) thy end;
+
+fun add_undefined c thy =
+  (map_exec_purge o map_cases o apsnd) (Symtab.update (c, ())) thy;
+
+
+(* datatypes *)
+
+structure Type_Interpretation =
+  Interpretation(type T = string * serial val eq = eq_snd (op =) : T * T -> bool);
+
+fun add_datatype raw_cs thy =
+  let
+    val cs = map (fn c_ty as (_, ty) => (AxClass.unoverload_const thy c_ty, ty)) raw_cs;
+    val (tyco, vs_cos) = constrset_of_consts thy cs;
+    val old_cs = (map fst o snd o get_datatype thy) tyco;
+    fun drop_outdated_cases cases = fold Symtab.delete_safe
+      (Symtab.fold (fn (c, (_, (_, cos))) =>
+        if exists (member (op =) old_cs) cos
+          then insert (op =) c else I) cases []) cases;
+  in
+    thy
+    |> fold (del_eqns o fst) cs
+    |> map_exec_purge
+        ((map_dtyps o Symtab.map_default (tyco, [])) (cons (serial (), vs_cos))
+        #> (map_cases o apfst) drop_outdated_cases)
+    |> Type_Interpretation.data (tyco, serial ())
+  end;
+
+fun type_interpretation f =  Type_Interpretation.interpretation
+  (fn (tyco, _) => fn thy => f (tyco, get_datatype thy tyco) thy);
+
+fun add_datatype_cmd raw_cs thy =
+  let
+    val cs = map (read_bare_const thy) raw_cs;
+  in add_datatype cs thy end;
+
+
 (* c.f. src/HOL/Tools/recfun_codegen.ML *)
 
 structure Code_Target_Attr = Theory_Data
@@ -789,7 +787,6 @@
   let
     val attr = the_default ((K o K) I) (Code_Target_Attr.get thy);
   in thy |> add_warning_eqn thm |> attr prefix thm end;
-
 (* setup *)
 
 val _ = Context.>> (Context.map_theory
@@ -807,21 +804,6 @@
         "declare theorems for code generation"
   end));
 
-
-(* cases *)
-
-fun add_case thm thy =
-  let
-    val (c, (k, case_pats)) = case_cert thm;
-    val _ = case filter_out (is_constr thy) case_pats
-     of [] => ()
-      | cs => error ("Non-constructor(s) in case certificate: " ^ commas (map quote cs));
-    val entry = (1 + Int.max (1, length case_pats), (k, case_pats))
-  in (map_exec_purge o map_cases o apfst) (Symtab.update (c, entry)) thy end;
-
-fun add_undefined c thy =
-  (map_exec_purge o map_cases o apsnd) (Symtab.update (c, ())) thy;
-
 end; (*struct*)
 
 
diff -r b28be884edda -r 54621a41b03c src/Pure/axclass.ML
--- a/src/Pure/axclass.ML	Mon Jan 04 11:55:23 2010 +0100
+++ b/src/Pure/axclass.ML	Mon Jan 04 14:10:13 2010 +0100
@@ -118,7 +118,6 @@
 (
   type T = axclasses * (instances * inst_params);
   val empty = ((Symtab.empty, []), (([], Symtab.empty), (Symtab.empty, Symtab.empty)));
-  val copy = I;
   val extend = I;
   fun merge pp ((axclasses1, (instances1, inst_params1)), (axclasses2, (instances2, inst_params2))) =
     (merge_axclasses pp (axclasses1, axclasses2),
diff -r b28be884edda -r 54621a41b03c src/Pure/context.ML
--- a/src/Pure/context.ML	Mon Jan 04 11:55:23 2010 +0100
+++ b/src/Pure/context.ML	Mon Jan 04 14:10:13 2010 +0100
@@ -83,7 +83,7 @@
   include CONTEXT
   structure Theory_Data:
   sig
-    val declare: Object.T -> (Object.T -> Object.T) -> (Object.T -> Object.T) ->
+    val declare: Object.T -> (Object.T -> Object.T) ->
       (Pretty.pp -> Object.T * Object.T -> Object.T) -> serial
     val get: serial -> (Object.T -> 'a) -> theory -> 'a
     val put: serial -> ('a -> Object.T) -> 'a -> theory -> theory
@@ -112,7 +112,6 @@
 
 type kind =
  {empty: Object.T,
-  copy: Object.T -> Object.T,
   extend: Object.T -> Object.T,
   merge: Pretty.pp -> Object.T * Object.T -> Object.T};
 
@@ -126,18 +125,16 @@
 in
 
 fun invoke_empty k = invoke (K o #empty) k ();
-val invoke_copy = invoke #copy;
 val invoke_extend = invoke #extend;
 fun invoke_merge pp = invoke (fn kind => #merge kind pp);
 
-fun declare_theory_data empty copy extend merge =
+fun declare_theory_data empty extend merge =
   let
     val k = serial ();
-    val kind = {empty = empty, copy = copy, extend = extend, merge = merge};
+    val kind = {empty = empty, extend = extend, merge = merge};
     val _ = CRITICAL (fn () => Unsynchronized.change kinds (Datatab.update (k, kind)));
   in k end;
 
-val copy_data = Datatab.map' invoke_copy;
 val extend_data = Datatab.map' invoke_extend;
 
 fun merge_data pp (data1, data2) =
@@ -341,7 +338,7 @@
     val (self', data', ancestry') =
       if draft then (self, data, ancestry)    (*destructive change!*)
       else if #stage history > 0
-      then (NONE, copy_data data, ancestry)
+      then (NONE, data, ancestry)
       else (NONE, extend_data data, make_ancestry [thy] (extend_ancestors_of thy));
     val ids' = insert_id draft id ids;
     val data'' = f data';
@@ -357,9 +354,8 @@
   let
     val Theory ({draft, id, ids, ...}, data, ancestry, history) = thy;
     val ids' = insert_id draft id ids;
-    val data' = copy_data data;
     val thy' = SYNCHRONIZED (fn () =>
-      (check_thy thy; create_thy NONE true ids' data' ancestry history));
+      (check_thy thy; create_thy NONE true ids' data ancestry history));
   in thy' end;
 
 val pre_pure_thy = create_thy NONE true Inttab.empty
@@ -430,9 +426,9 @@
 val declare = declare_theory_data;
 
 fun get k dest thy =
-  dest ((case Datatab.lookup (data_of thy) k of
+  dest (case Datatab.lookup (data_of thy) k of
     SOME x => x
-  | NONE => invoke_copy k (invoke_empty k)));   (*adhoc value*)
+  | NONE => invoke_empty k);   (*adhoc value*)
 
 fun put k mk x = modify_thy (Datatab.update (k, mk x));
 
@@ -582,7 +578,6 @@
 sig
   type T
   val empty: T
-  val copy: T -> T
   val extend: T -> T
   val merge: Pretty.pp -> T * T -> T
 end;
@@ -604,7 +599,6 @@
 
 val kind = Context.Theory_Data.declare
   (Data Data.empty)
-  (fn Data x => Data (Data.copy x))
   (fn Data x => Data (Data.extend x))
   (fn pp => fn (Data x1, Data x2) => Data (Data.merge pp (x1, x2)));
 
@@ -639,7 +633,6 @@
 (
   type T = Data.T;
   val empty = Data.empty;
-  val copy = I;
   val extend = Data.extend;
   fun merge _ = Data.merge;
 );
diff -r b28be884edda -r 54621a41b03c src/Pure/sign.ML
--- a/src/Pure/sign.ML	Mon Jan 04 11:55:23 2010 +0100
+++ b/src/Pure/sign.ML	Mon Jan 04 14:10:13 2010 +0100
@@ -151,7 +151,6 @@
 structure SignData = TheoryDataFun
 (
   type T = sign;
-  val copy = I;
   fun extend (Sign {syn, tsig, consts, ...}) =
     make_sign (Name_Space.default_naming, syn, tsig, consts);
 
diff -r b28be884edda -r 54621a41b03c src/Pure/theory.ML
--- a/src/Pure/theory.ML	Mon Jan 04 11:55:23 2010 +0100
+++ b/src/Pure/theory.ML	Mon Jan 04 14:10:13 2010 +0100
@@ -91,7 +91,6 @@
   type T = thy;
   val empty_axioms = Name_Space.empty_table "axiom" : term Name_Space.table;
   val empty = make_thy (empty_axioms, Defs.empty, ([], []));
-  val copy = I;
 
   fun extend (Thy {axioms = _, defs, wrappers}) = make_thy (empty_axioms, defs, wrappers);
 
diff -r b28be884edda -r 54621a41b03c src/Tools/Code/code_ml.ML
--- a/src/Tools/Code/code_ml.ML	Mon Jan 04 11:55:23 2010 +0100
+++ b/src/Tools/Code/code_ml.ML	Mon Jan 04 14:10:13 2010 +0100
@@ -481,8 +481,6 @@
               let
                 val consts = fold Code_Thingol.add_constnames (t :: ts) [];
                 val vars = reserved
-                  |> intro_base_names
-                      (is_none o syntax_const) deresolve consts
                   |> intro_vars ((fold o Code_Thingol.fold_varnames)
                       (insert (op =)) ts []);
               in concat [
diff -r b28be884edda -r 54621a41b03c src/Tools/Code/code_preproc.ML
--- a/src/Tools/Code/code_preproc.ML	Mon Jan 04 11:55:23 2010 +0100
+++ b/src/Tools/Code/code_preproc.ML	Mon Jan 04 14:10:13 2010 +0100
@@ -454,8 +454,8 @@
 
 (** retrieval and evaluation interfaces **)
 
-fun obtain thy cs ts = apsnd snd
-  (Wellsorted.change_yield thy (extend_arities_eqngr thy cs ts));
+fun obtain theory cs ts = apsnd snd
+  (Wellsorted.change_yield theory (fn thy => extend_arities_eqngr thy cs ts));
 
 fun gen_eval thy cterm_of conclude_evaluation evaluator proto_ct =
   let
diff -r b28be884edda -r 54621a41b03c src/Tools/Code/code_printer.ML
--- a/src/Tools/Code/code_printer.ML	Mon Jan 04 11:55:23 2010 +0100
+++ b/src/Tools/Code/code_printer.ML	Mon Jan 04 14:10:13 2010 +0100
@@ -60,6 +60,7 @@
   val brackify: fixity -> Pretty.T list -> Pretty.T
   val brackify_infix: int * lrx -> fixity -> Pretty.T list -> Pretty.T
   val brackify_block: fixity -> Pretty.T -> Pretty.T list -> Pretty.T -> Pretty.T
+  val applify: string -> string -> fixity -> Pretty.T -> Pretty.T list -> Pretty.T
 
   type tyco_syntax
   type simple_const_syntax
@@ -220,6 +221,11 @@
     else p
   end;
 
+fun applify opn cls fxy_ctxt p [] = p
+  | applify opn cls fxy_ctxt p ps =
+      (if (fixity BR fxy_ctxt) then enclose "(" ")" else Pretty.block)
+        (p @@ enum "," opn cls ps);
+
 
 (* generic syntax *)
 
diff -r b28be884edda -r 54621a41b03c src/Tools/Code/code_target.ML
--- a/src/Tools/Code/code_target.ML	Mon Jan 04 11:55:23 2010 +0100
+++ b/src/Tools/Code/code_target.ML	Mon Jan 04 14:10:13 2010 +0100
@@ -153,7 +153,7 @@
 fun the_name_syntax (Target { name_syntax_table = NameSyntaxTable x, ... }) = x;
 fun the_module_alias (Target { module_alias , ... }) = module_alias;
 
-structure CodeTargetData = Theory_Data
+structure Targets = Theory_Data
 (
   type T = (target Symtab.table * string list) * int;
   val empty = ((Symtab.empty, []), 80);
@@ -163,17 +163,17 @@
       Library.merge (op =) (exc1, exc2)), Int.max (width1, width2));
 );
 
-val abort_allowed = snd o fst o CodeTargetData.get;
+val abort_allowed = snd o fst o Targets.get;
 
-val the_default_width = snd o CodeTargetData.get;
+val the_default_width = snd o Targets.get;
 
-fun assert_target thy target = if Symtab.defined ((fst o fst) (CodeTargetData.get thy)) target
+fun assert_target thy target = if Symtab.defined ((fst o fst) (Targets.get thy)) target
   then target
   else error ("Unknown code target language: " ^ quote target);
 
 fun put_target (target, seri) thy =
   let
-    val lookup_target = Symtab.lookup ((fst o fst) (CodeTargetData.get thy));
+    val lookup_target = Symtab.lookup ((fst o fst) (Targets.get thy));
     val _ = case seri
      of Extends (super, _) => if is_some (lookup_target super) then ()
           else error ("Unknown code target language: " ^ quote super)
@@ -189,11 +189,10 @@
       else (); 
   in
     thy
-    |> (CodeTargetData.map o apfst o apfst oo Symtab.map_default)
+    |> (Targets.map o apfst o apfst o Symtab.update)
           (target, make_target ((serial (), seri), (([], Symtab.empty),
             (mk_name_syntax_table ((Symtab.empty, Symreltab.empty), (Symtab.empty, Symtab.empty)),
               Symtab.empty))))
-          ((map_target o apfst o apsnd o K) seri)
   end;
 
 fun add_target (target, seri) = put_target (target, Serializer seri);
@@ -205,7 +204,7 @@
     val _ = assert_target thy target;
   in
     thy
-    |> (CodeTargetData.map o apfst o apfst o Symtab.map_entry target o map_target) f
+    |> (Targets.map o apfst o apfst o Symtab.map_entry target o map_target) f
   end;
 
 fun map_reserved target =
@@ -217,7 +216,7 @@
 fun map_module_alias target =
   map_target_data target o apsnd o apsnd o apsnd;
 
-fun set_default_code_width k = (CodeTargetData.map o apsnd) (K k);
+fun set_default_code_width k = (Targets.map o apsnd) (K k);
 
 
 (** serializer usage **)
@@ -226,7 +225,7 @@
 
 fun the_literals thy =
   let
-    val ((targets, _), _) = CodeTargetData.get thy;
+    val ((targets, _), _) = Targets.get thy;
     fun literals target = case Symtab.lookup targets target
      of SOME data => (case the_serializer data
          of Serializer (_, literals) => literals
@@ -284,7 +283,7 @@
 
 fun mount_serializer thy alt_serializer target some_width module args naming program names =
   let
-    val ((targets, abortable), default_width) = CodeTargetData.get thy;
+    val ((targets, abortable), default_width) = Targets.get thy;
     fun collapse_hierarchy target =
       let
         val data = case Symtab.lookup targets target
@@ -457,7 +456,7 @@
 fun gen_allow_abort prep_const raw_c thy =
   let
     val c = prep_const thy raw_c;
-  in thy |> (CodeTargetData.map o apfst o apsnd) (insert (op =) c) end;
+  in thy |> (Targets.map o apfst o apsnd) (insert (op =) c) end;
 
 
 (* concrete syntax *)
diff -r b28be884edda -r 54621a41b03c src/Tools/Code/code_thingol.ML
--- a/src/Tools/Code/code_thingol.ML	Mon Jan 04 11:55:23 2010 +0100
+++ b/src/Tools/Code/code_thingol.ML	Mon Jan 04 14:10:13 2010 +0100
@@ -848,8 +848,8 @@
   val empty = (empty_naming, Graph.empty);
 );
 
-fun invoke_generation thy (algebra, eqngr) f name =
-  Program.change_yield thy (fn naming_program => (NONE, naming_program)
+fun invoke_generation theory (algebra, eqngr) f name =
+  Program.change_yield theory (fn thy => fn naming_program => (NONE, naming_program)
     |> f thy algebra eqngr name
     |-> (fn name => fn (_, naming_program) => (name, naming_program)));
 
diff -r b28be884edda -r 54621a41b03c src/Tools/nbe.ML
--- a/src/Tools/nbe.ML	Mon Jan 04 11:55:23 2010 +0100
+++ b/src/Tools/nbe.ML	Mon Jan 04 14:10:13 2010 +0100
@@ -513,15 +513,14 @@
 
 (* compilation, evaluation and reification *)
 
-fun compile_eval thy naming program vs_t deps =
+fun compile_eval theory naming program vs_t deps =
   let
-    val ctxt = ProofContext.init thy;
     val (_, (gr, (_, idx_tab))) =
-      Nbe_Functions.change thy (ensure_stmts ctxt naming program o snd);
+      Nbe_Functions.change theory (fn thy => ensure_stmts (ProofContext.init thy) naming program o snd);
   in
     vs_t
-    |> eval_term ctxt gr deps
-    |> term_of_univ thy program idx_tab
+    |> eval_term (ProofContext.init theory) gr deps
+    |> term_of_univ theory program idx_tab
   end;
 
 (* evaluation with type reconstruction *)