merged
authorhaftmann
Mon Jan 04 14:10:13 2010 +0100 (2010-01-04)
changeset 3424954621a41b03c
parent 34238 b28be884edda
parent 34248 6fb7dd3fd81a
child 34250 3b619abaa67a
merged
     1.1 --- a/src/Pure/Isar/code.ML	Mon Jan 04 11:55:23 2010 +0100
     1.2 +++ b/src/Pure/Isar/code.ML	Mon Jan 04 14:10:13 2010 +0100
     1.3 @@ -76,8 +76,8 @@
     1.4  signature CODE_DATA =
     1.5  sig
     1.6    type T
     1.7 -  val change: theory -> (T -> T) -> T
     1.8 -  val change_yield: theory -> (T -> 'a * T) -> 'a * T
     1.9 +  val change: theory -> (theory -> T -> T) -> T
    1.10 +  val change_yield: theory -> (theory -> T -> 'a * T) -> 'a * T
    1.11  end;
    1.12  
    1.13  signature PRIVATE_CODE =
    1.14 @@ -85,9 +85,9 @@
    1.15    include CODE
    1.16    val declare_data: Object.T -> serial
    1.17    val change_data: serial * ('a -> Object.T) * (Object.T -> 'a)
    1.18 -    -> theory -> ('a -> 'a) -> 'a
    1.19 +    -> theory -> (theory -> 'a -> 'a) -> 'a
    1.20    val change_yield_data: serial * ('a -> Object.T) * (Object.T -> 'a)
    1.21 -    -> theory -> ('a -> 'b * 'a) -> 'b * 'a
    1.22 +    -> theory -> (theory -> 'a -> 'b * 'a) -> 'b * 'a
    1.23  end;
    1.24  
    1.25  structure Code : PRIVATE_CODE =
    1.26 @@ -234,53 +234,35 @@
    1.27  local
    1.28  
    1.29  type data = Object.T Datatab.table;
    1.30 -fun create_data data = Synchronized.var "code data" data;
    1.31 -fun empty_data () = create_data Datatab.empty : data Synchronized.var;
    1.32 +fun empty_dataref () = Synchronized.var "code data" (NONE : (data * theory_ref) option);
    1.33  
    1.34 -structure Code_Data = TheoryDataFun
    1.35 +structure Code_Data = Theory_Data
    1.36  (
    1.37 -  type T = spec * data Synchronized.var;
    1.38 +  type T = spec * (data * theory_ref) option Synchronized.var;
    1.39    val empty = (make_spec (false, (((Symtab.empty, Symtab.empty), Symtab.empty),
    1.40 -    (Symtab.empty, (Symtab.empty, Symtab.empty)))), empty_data ());
    1.41 -  fun copy (spec, data) = (spec, create_data (Synchronized.value data));
    1.42 -  val extend = copy;
    1.43 -  fun merge _ ((spec1, _), (spec2, _)) =
    1.44 -    (merge_spec (spec1, spec2), empty_data ());
    1.45 +    (Symtab.empty, (Symtab.empty, Symtab.empty)))), empty_dataref ());
    1.46 +  val extend = I
    1.47 +  fun merge ((spec1, _), (spec2, _)) =
    1.48 +    (merge_spec (spec1, spec2), empty_dataref ());
    1.49  );
    1.50  
    1.51 -fun thy_data f thy = f ((snd o Code_Data.get) thy);
    1.52 -
    1.53 -fun get_ensure_init kind data =
    1.54 -  case Datatab.lookup (Synchronized.value data) kind
    1.55 -   of SOME x => x
    1.56 -    | NONE => let val y = invoke_init kind
    1.57 -        in (Synchronized.change data (Datatab.update (kind, y)); y) end;
    1.58 -
    1.59  in
    1.60  
    1.61  (* access to executable code *)
    1.62  
    1.63  val the_exec = fst o Code_Data.get;
    1.64  
    1.65 -fun map_exec_purge f =
    1.66 -  Code_Data.map (fn (exec, data) => (f exec, empty_data ()));
    1.67 +fun map_exec_purge f = Code_Data.map (fn (exec, _) => (f exec, empty_dataref ()));
    1.68  
    1.69 -val purge_data = (Code_Data.map o apsnd) (fn _ => empty_data ());
    1.70 +val purge_data = (Code_Data.map o apsnd) (fn _ => empty_dataref ());
    1.71  
    1.72  fun change_eqns delete c f = (map_exec_purge o map_eqns
    1.73    o (if delete then Symtab.map_entry c else Symtab.map_default (c, ((false, (true, [])), [])))
    1.74      o apfst) (fn (_, eqns) => (true, f eqns));
    1.75  
    1.76 -fun del_eqns c = change_eqns true c (K (false, []));
    1.77 -
    1.78  
    1.79  (* tackling equation history *)
    1.80  
    1.81 -fun get_eqns thy c =
    1.82 -  Symtab.lookup ((the_eqns o the_exec) thy) c
    1.83 -  |> Option.map (snd o snd o fst)
    1.84 -  |> these;
    1.85 -
    1.86  fun continue_history thy = if (history_concluded o the_exec) thy
    1.87    then thy
    1.88      |> (Code_Data.map o apfst o map_history_concluded) (K false)
    1.89 @@ -297,30 +279,26 @@
    1.90          #> map_history_concluded (K true))
    1.91      |> SOME;
    1.92  
    1.93 -val _ = Context.>> (Context.map_theory (Code_Data.init
    1.94 -  #> Theory.at_begin continue_history
    1.95 -  #> Theory.at_end conclude_history));
    1.96 +val _ = Context.>> (Context.map_theory (Theory.at_begin continue_history #> Theory.at_end conclude_history));
    1.97  
    1.98  
    1.99  (* access to data dependent on abstract executable code *)
   1.100  
   1.101 -fun change_data (kind, mk, dest) =
   1.102 +fun change_yield_data (kind, mk, dest) theory f =
   1.103    let
   1.104 -    fun chnge data_ref f =
   1.105 -      let
   1.106 -        val data = get_ensure_init kind data_ref;
   1.107 -        val data' = f (dest data);
   1.108 -      in (Synchronized.change data_ref (Datatab.update (kind, mk data')); data') end;
   1.109 -  in thy_data chnge end;
   1.110 +    val dataref = (snd o Code_Data.get) theory;
   1.111 +    val (datatab, thy, thy_ref) = case Synchronized.value dataref
   1.112 +     of SOME (datatab, thy_ref) => (datatab, Theory.deref thy_ref, thy_ref)
   1.113 +      | NONE => (Datatab.empty, theory, Theory.check_thy theory)
   1.114 +    val data = case Datatab.lookup datatab kind
   1.115 +     of SOME data => data
   1.116 +      | NONE => invoke_init kind;
   1.117 +    val result as (x, data') = f thy (dest data);
   1.118 +    val _ = Synchronized.change dataref
   1.119 +      ((K o SOME) (Datatab.update (kind, mk data') datatab, thy_ref));
   1.120 +  in result end;
   1.121  
   1.122 -fun change_yield_data (kind, mk, dest) =
   1.123 -  let
   1.124 -    fun chnge data_ref f =
   1.125 -      let
   1.126 -        val data = get_ensure_init kind data_ref;
   1.127 -        val (x, data') = f (dest data);
   1.128 -      in (x, (Synchronized.change data_ref (Datatab.update (kind, mk data')); data')) end;
   1.129 -  in thy_data chnge end;
   1.130 +fun change_data ops theory f = change_yield_data ops theory (pair () oo f) |> snd;
   1.131  
   1.132  end; (*local*)
   1.133  
   1.134 @@ -574,7 +552,9 @@
   1.135    in map2 (fn vs => Thm.certify_instantiate (vs ~~ vts, [])) vss thms end;
   1.136  
   1.137  fun these_eqns thy c =
   1.138 -  get_eqns thy c
   1.139 +  Symtab.lookup ((the_eqns o the_exec) thy) c
   1.140 +  |> Option.map (snd o snd o fst)
   1.141 +  |> these
   1.142    |> (map o apfst) (Thm.transfer thy)
   1.143    |> burrow_fst (standard_typscheme thy);
   1.144  
   1.145 @@ -709,38 +689,6 @@
   1.146  val add_signature_cmd = gen_add_signature read_const read_signature;
   1.147  
   1.148  
   1.149 -(* datatypes *)
   1.150 -
   1.151 -structure Type_Interpretation =
   1.152 -  Interpretation(type T = string * serial val eq = eq_snd (op =) : T * T -> bool);
   1.153 -
   1.154 -fun add_datatype raw_cs thy =
   1.155 -  let
   1.156 -    val cs = map (fn c_ty as (_, ty) => (AxClass.unoverload_const thy c_ty, ty)) raw_cs;
   1.157 -    val (tyco, vs_cos) = constrset_of_consts thy cs;
   1.158 -    val old_cs = (map fst o snd o get_datatype thy) tyco;
   1.159 -    fun drop_outdated_cases cases = fold Symtab.delete_safe
   1.160 -      (Symtab.fold (fn (c, (_, (_, cos))) =>
   1.161 -        if exists (member (op =) old_cs) cos
   1.162 -          then insert (op =) c else I) cases []) cases;
   1.163 -  in
   1.164 -    thy
   1.165 -    |> fold (del_eqns o fst) cs
   1.166 -    |> map_exec_purge
   1.167 -        ((map_dtyps o Symtab.map_default (tyco, [])) (cons (serial (), vs_cos))
   1.168 -        #> (map_cases o apfst) drop_outdated_cases)
   1.169 -    |> Type_Interpretation.data (tyco, serial ())
   1.170 -  end;
   1.171 -
   1.172 -fun type_interpretation f =  Type_Interpretation.interpretation
   1.173 -  (fn (tyco, _) => fn thy => f (tyco, get_datatype thy tyco) thy);
   1.174 -
   1.175 -fun add_datatype_cmd raw_cs thy =
   1.176 -  let
   1.177 -    val cs = map (read_bare_const thy) raw_cs;
   1.178 -  in add_datatype cs thy end;
   1.179 -
   1.180 -
   1.181  (* code equations *)
   1.182  
   1.183  fun gen_add_eqn default (thm, proper) thy =
   1.184 @@ -773,6 +721,56 @@
   1.185   of SOME (thm, _) => change_eqns true (const_eqn thy thm) (del_thm thm) thy
   1.186    | NONE => thy;
   1.187  
   1.188 +fun del_eqns c = change_eqns true c (K (false, []));
   1.189 +
   1.190 +
   1.191 +(* cases *)
   1.192 +
   1.193 +fun add_case thm thy =
   1.194 +  let
   1.195 +    val (c, (k, case_pats)) = case_cert thm;
   1.196 +    val _ = case filter_out (is_constr thy) case_pats
   1.197 +     of [] => ()
   1.198 +      | cs => error ("Non-constructor(s) in case certificate: " ^ commas (map quote cs));
   1.199 +    val entry = (1 + Int.max (1, length case_pats), (k, case_pats))
   1.200 +  in (map_exec_purge o map_cases o apfst) (Symtab.update (c, entry)) thy end;
   1.201 +
   1.202 +fun add_undefined c thy =
   1.203 +  (map_exec_purge o map_cases o apsnd) (Symtab.update (c, ())) thy;
   1.204 +
   1.205 +
   1.206 +(* datatypes *)
   1.207 +
   1.208 +structure Type_Interpretation =
   1.209 +  Interpretation(type T = string * serial val eq = eq_snd (op =) : T * T -> bool);
   1.210 +
   1.211 +fun add_datatype raw_cs thy =
   1.212 +  let
   1.213 +    val cs = map (fn c_ty as (_, ty) => (AxClass.unoverload_const thy c_ty, ty)) raw_cs;
   1.214 +    val (tyco, vs_cos) = constrset_of_consts thy cs;
   1.215 +    val old_cs = (map fst o snd o get_datatype thy) tyco;
   1.216 +    fun drop_outdated_cases cases = fold Symtab.delete_safe
   1.217 +      (Symtab.fold (fn (c, (_, (_, cos))) =>
   1.218 +        if exists (member (op =) old_cs) cos
   1.219 +          then insert (op =) c else I) cases []) cases;
   1.220 +  in
   1.221 +    thy
   1.222 +    |> fold (del_eqns o fst) cs
   1.223 +    |> map_exec_purge
   1.224 +        ((map_dtyps o Symtab.map_default (tyco, [])) (cons (serial (), vs_cos))
   1.225 +        #> (map_cases o apfst) drop_outdated_cases)
   1.226 +    |> Type_Interpretation.data (tyco, serial ())
   1.227 +  end;
   1.228 +
   1.229 +fun type_interpretation f =  Type_Interpretation.interpretation
   1.230 +  (fn (tyco, _) => fn thy => f (tyco, get_datatype thy tyco) thy);
   1.231 +
   1.232 +fun add_datatype_cmd raw_cs thy =
   1.233 +  let
   1.234 +    val cs = map (read_bare_const thy) raw_cs;
   1.235 +  in add_datatype cs thy end;
   1.236 +
   1.237 +
   1.238  (* c.f. src/HOL/Tools/recfun_codegen.ML *)
   1.239  
   1.240  structure Code_Target_Attr = Theory_Data
   1.241 @@ -789,7 +787,6 @@
   1.242    let
   1.243      val attr = the_default ((K o K) I) (Code_Target_Attr.get thy);
   1.244    in thy |> add_warning_eqn thm |> attr prefix thm end;
   1.245 -
   1.246  (* setup *)
   1.247  
   1.248  val _ = Context.>> (Context.map_theory
   1.249 @@ -807,21 +804,6 @@
   1.250          "declare theorems for code generation"
   1.251    end));
   1.252  
   1.253 -
   1.254 -(* cases *)
   1.255 -
   1.256 -fun add_case thm thy =
   1.257 -  let
   1.258 -    val (c, (k, case_pats)) = case_cert thm;
   1.259 -    val _ = case filter_out (is_constr thy) case_pats
   1.260 -     of [] => ()
   1.261 -      | cs => error ("Non-constructor(s) in case certificate: " ^ commas (map quote cs));
   1.262 -    val entry = (1 + Int.max (1, length case_pats), (k, case_pats))
   1.263 -  in (map_exec_purge o map_cases o apfst) (Symtab.update (c, entry)) thy end;
   1.264 -
   1.265 -fun add_undefined c thy =
   1.266 -  (map_exec_purge o map_cases o apsnd) (Symtab.update (c, ())) thy;
   1.267 -
   1.268  end; (*struct*)
   1.269  
   1.270  
     2.1 --- a/src/Pure/axclass.ML	Mon Jan 04 11:55:23 2010 +0100
     2.2 +++ b/src/Pure/axclass.ML	Mon Jan 04 14:10:13 2010 +0100
     2.3 @@ -118,7 +118,6 @@
     2.4  (
     2.5    type T = axclasses * (instances * inst_params);
     2.6    val empty = ((Symtab.empty, []), (([], Symtab.empty), (Symtab.empty, Symtab.empty)));
     2.7 -  val copy = I;
     2.8    val extend = I;
     2.9    fun merge pp ((axclasses1, (instances1, inst_params1)), (axclasses2, (instances2, inst_params2))) =
    2.10      (merge_axclasses pp (axclasses1, axclasses2),
     3.1 --- a/src/Pure/context.ML	Mon Jan 04 11:55:23 2010 +0100
     3.2 +++ b/src/Pure/context.ML	Mon Jan 04 14:10:13 2010 +0100
     3.3 @@ -83,7 +83,7 @@
     3.4    include CONTEXT
     3.5    structure Theory_Data:
     3.6    sig
     3.7 -    val declare: Object.T -> (Object.T -> Object.T) -> (Object.T -> Object.T) ->
     3.8 +    val declare: Object.T -> (Object.T -> Object.T) ->
     3.9        (Pretty.pp -> Object.T * Object.T -> Object.T) -> serial
    3.10      val get: serial -> (Object.T -> 'a) -> theory -> 'a
    3.11      val put: serial -> ('a -> Object.T) -> 'a -> theory -> theory
    3.12 @@ -112,7 +112,6 @@
    3.13  
    3.14  type kind =
    3.15   {empty: Object.T,
    3.16 -  copy: Object.T -> Object.T,
    3.17    extend: Object.T -> Object.T,
    3.18    merge: Pretty.pp -> Object.T * Object.T -> Object.T};
    3.19  
    3.20 @@ -126,18 +125,16 @@
    3.21  in
    3.22  
    3.23  fun invoke_empty k = invoke (K o #empty) k ();
    3.24 -val invoke_copy = invoke #copy;
    3.25  val invoke_extend = invoke #extend;
    3.26  fun invoke_merge pp = invoke (fn kind => #merge kind pp);
    3.27  
    3.28 -fun declare_theory_data empty copy extend merge =
    3.29 +fun declare_theory_data empty extend merge =
    3.30    let
    3.31      val k = serial ();
    3.32 -    val kind = {empty = empty, copy = copy, extend = extend, merge = merge};
    3.33 +    val kind = {empty = empty, extend = extend, merge = merge};
    3.34      val _ = CRITICAL (fn () => Unsynchronized.change kinds (Datatab.update (k, kind)));
    3.35    in k end;
    3.36  
    3.37 -val copy_data = Datatab.map' invoke_copy;
    3.38  val extend_data = Datatab.map' invoke_extend;
    3.39  
    3.40  fun merge_data pp (data1, data2) =
    3.41 @@ -341,7 +338,7 @@
    3.42      val (self', data', ancestry') =
    3.43        if draft then (self, data, ancestry)    (*destructive change!*)
    3.44        else if #stage history > 0
    3.45 -      then (NONE, copy_data data, ancestry)
    3.46 +      then (NONE, data, ancestry)
    3.47        else (NONE, extend_data data, make_ancestry [thy] (extend_ancestors_of thy));
    3.48      val ids' = insert_id draft id ids;
    3.49      val data'' = f data';
    3.50 @@ -357,9 +354,8 @@
    3.51    let
    3.52      val Theory ({draft, id, ids, ...}, data, ancestry, history) = thy;
    3.53      val ids' = insert_id draft id ids;
    3.54 -    val data' = copy_data data;
    3.55      val thy' = SYNCHRONIZED (fn () =>
    3.56 -      (check_thy thy; create_thy NONE true ids' data' ancestry history));
    3.57 +      (check_thy thy; create_thy NONE true ids' data ancestry history));
    3.58    in thy' end;
    3.59  
    3.60  val pre_pure_thy = create_thy NONE true Inttab.empty
    3.61 @@ -430,9 +426,9 @@
    3.62  val declare = declare_theory_data;
    3.63  
    3.64  fun get k dest thy =
    3.65 -  dest ((case Datatab.lookup (data_of thy) k of
    3.66 +  dest (case Datatab.lookup (data_of thy) k of
    3.67      SOME x => x
    3.68 -  | NONE => invoke_copy k (invoke_empty k)));   (*adhoc value*)
    3.69 +  | NONE => invoke_empty k);   (*adhoc value*)
    3.70  
    3.71  fun put k mk x = modify_thy (Datatab.update (k, mk x));
    3.72  
    3.73 @@ -582,7 +578,6 @@
    3.74  sig
    3.75    type T
    3.76    val empty: T
    3.77 -  val copy: T -> T
    3.78    val extend: T -> T
    3.79    val merge: Pretty.pp -> T * T -> T
    3.80  end;
    3.81 @@ -604,7 +599,6 @@
    3.82  
    3.83  val kind = Context.Theory_Data.declare
    3.84    (Data Data.empty)
    3.85 -  (fn Data x => Data (Data.copy x))
    3.86    (fn Data x => Data (Data.extend x))
    3.87    (fn pp => fn (Data x1, Data x2) => Data (Data.merge pp (x1, x2)));
    3.88  
    3.89 @@ -639,7 +633,6 @@
    3.90  (
    3.91    type T = Data.T;
    3.92    val empty = Data.empty;
    3.93 -  val copy = I;
    3.94    val extend = Data.extend;
    3.95    fun merge _ = Data.merge;
    3.96  );
     4.1 --- a/src/Pure/sign.ML	Mon Jan 04 11:55:23 2010 +0100
     4.2 +++ b/src/Pure/sign.ML	Mon Jan 04 14:10:13 2010 +0100
     4.3 @@ -151,7 +151,6 @@
     4.4  structure SignData = TheoryDataFun
     4.5  (
     4.6    type T = sign;
     4.7 -  val copy = I;
     4.8    fun extend (Sign {syn, tsig, consts, ...}) =
     4.9      make_sign (Name_Space.default_naming, syn, tsig, consts);
    4.10  
     5.1 --- a/src/Pure/theory.ML	Mon Jan 04 11:55:23 2010 +0100
     5.2 +++ b/src/Pure/theory.ML	Mon Jan 04 14:10:13 2010 +0100
     5.3 @@ -91,7 +91,6 @@
     5.4    type T = thy;
     5.5    val empty_axioms = Name_Space.empty_table "axiom" : term Name_Space.table;
     5.6    val empty = make_thy (empty_axioms, Defs.empty, ([], []));
     5.7 -  val copy = I;
     5.8  
     5.9    fun extend (Thy {axioms = _, defs, wrappers}) = make_thy (empty_axioms, defs, wrappers);
    5.10  
     6.1 --- a/src/Tools/Code/code_ml.ML	Mon Jan 04 11:55:23 2010 +0100
     6.2 +++ b/src/Tools/Code/code_ml.ML	Mon Jan 04 14:10:13 2010 +0100
     6.3 @@ -481,8 +481,6 @@
     6.4                let
     6.5                  val consts = fold Code_Thingol.add_constnames (t :: ts) [];
     6.6                  val vars = reserved
     6.7 -                  |> intro_base_names
     6.8 -                      (is_none o syntax_const) deresolve consts
     6.9                    |> intro_vars ((fold o Code_Thingol.fold_varnames)
    6.10                        (insert (op =)) ts []);
    6.11                in concat [
     7.1 --- a/src/Tools/Code/code_preproc.ML	Mon Jan 04 11:55:23 2010 +0100
     7.2 +++ b/src/Tools/Code/code_preproc.ML	Mon Jan 04 14:10:13 2010 +0100
     7.3 @@ -454,8 +454,8 @@
     7.4  
     7.5  (** retrieval and evaluation interfaces **)
     7.6  
     7.7 -fun obtain thy cs ts = apsnd snd
     7.8 -  (Wellsorted.change_yield thy (extend_arities_eqngr thy cs ts));
     7.9 +fun obtain theory cs ts = apsnd snd
    7.10 +  (Wellsorted.change_yield theory (fn thy => extend_arities_eqngr thy cs ts));
    7.11  
    7.12  fun gen_eval thy cterm_of conclude_evaluation evaluator proto_ct =
    7.13    let
     8.1 --- a/src/Tools/Code/code_printer.ML	Mon Jan 04 11:55:23 2010 +0100
     8.2 +++ b/src/Tools/Code/code_printer.ML	Mon Jan 04 14:10:13 2010 +0100
     8.3 @@ -60,6 +60,7 @@
     8.4    val brackify: fixity -> Pretty.T list -> Pretty.T
     8.5    val brackify_infix: int * lrx -> fixity -> Pretty.T list -> Pretty.T
     8.6    val brackify_block: fixity -> Pretty.T -> Pretty.T list -> Pretty.T -> Pretty.T
     8.7 +  val applify: string -> string -> fixity -> Pretty.T -> Pretty.T list -> Pretty.T
     8.8  
     8.9    type tyco_syntax
    8.10    type simple_const_syntax
    8.11 @@ -220,6 +221,11 @@
    8.12      else p
    8.13    end;
    8.14  
    8.15 +fun applify opn cls fxy_ctxt p [] = p
    8.16 +  | applify opn cls fxy_ctxt p ps =
    8.17 +      (if (fixity BR fxy_ctxt) then enclose "(" ")" else Pretty.block)
    8.18 +        (p @@ enum "," opn cls ps);
    8.19 +
    8.20  
    8.21  (* generic syntax *)
    8.22  
     9.1 --- a/src/Tools/Code/code_target.ML	Mon Jan 04 11:55:23 2010 +0100
     9.2 +++ b/src/Tools/Code/code_target.ML	Mon Jan 04 14:10:13 2010 +0100
     9.3 @@ -153,7 +153,7 @@
     9.4  fun the_name_syntax (Target { name_syntax_table = NameSyntaxTable x, ... }) = x;
     9.5  fun the_module_alias (Target { module_alias , ... }) = module_alias;
     9.6  
     9.7 -structure CodeTargetData = Theory_Data
     9.8 +structure Targets = Theory_Data
     9.9  (
    9.10    type T = (target Symtab.table * string list) * int;
    9.11    val empty = ((Symtab.empty, []), 80);
    9.12 @@ -163,17 +163,17 @@
    9.13        Library.merge (op =) (exc1, exc2)), Int.max (width1, width2));
    9.14  );
    9.15  
    9.16 -val abort_allowed = snd o fst o CodeTargetData.get;
    9.17 +val abort_allowed = snd o fst o Targets.get;
    9.18  
    9.19 -val the_default_width = snd o CodeTargetData.get;
    9.20 +val the_default_width = snd o Targets.get;
    9.21  
    9.22 -fun assert_target thy target = if Symtab.defined ((fst o fst) (CodeTargetData.get thy)) target
    9.23 +fun assert_target thy target = if Symtab.defined ((fst o fst) (Targets.get thy)) target
    9.24    then target
    9.25    else error ("Unknown code target language: " ^ quote target);
    9.26  
    9.27  fun put_target (target, seri) thy =
    9.28    let
    9.29 -    val lookup_target = Symtab.lookup ((fst o fst) (CodeTargetData.get thy));
    9.30 +    val lookup_target = Symtab.lookup ((fst o fst) (Targets.get thy));
    9.31      val _ = case seri
    9.32       of Extends (super, _) => if is_some (lookup_target super) then ()
    9.33            else error ("Unknown code target language: " ^ quote super)
    9.34 @@ -189,11 +189,10 @@
    9.35        else (); 
    9.36    in
    9.37      thy
    9.38 -    |> (CodeTargetData.map o apfst o apfst oo Symtab.map_default)
    9.39 +    |> (Targets.map o apfst o apfst o Symtab.update)
    9.40            (target, make_target ((serial (), seri), (([], Symtab.empty),
    9.41              (mk_name_syntax_table ((Symtab.empty, Symreltab.empty), (Symtab.empty, Symtab.empty)),
    9.42                Symtab.empty))))
    9.43 -          ((map_target o apfst o apsnd o K) seri)
    9.44    end;
    9.45  
    9.46  fun add_target (target, seri) = put_target (target, Serializer seri);
    9.47 @@ -205,7 +204,7 @@
    9.48      val _ = assert_target thy target;
    9.49    in
    9.50      thy
    9.51 -    |> (CodeTargetData.map o apfst o apfst o Symtab.map_entry target o map_target) f
    9.52 +    |> (Targets.map o apfst o apfst o Symtab.map_entry target o map_target) f
    9.53    end;
    9.54  
    9.55  fun map_reserved target =
    9.56 @@ -217,7 +216,7 @@
    9.57  fun map_module_alias target =
    9.58    map_target_data target o apsnd o apsnd o apsnd;
    9.59  
    9.60 -fun set_default_code_width k = (CodeTargetData.map o apsnd) (K k);
    9.61 +fun set_default_code_width k = (Targets.map o apsnd) (K k);
    9.62  
    9.63  
    9.64  (** serializer usage **)
    9.65 @@ -226,7 +225,7 @@
    9.66  
    9.67  fun the_literals thy =
    9.68    let
    9.69 -    val ((targets, _), _) = CodeTargetData.get thy;
    9.70 +    val ((targets, _), _) = Targets.get thy;
    9.71      fun literals target = case Symtab.lookup targets target
    9.72       of SOME data => (case the_serializer data
    9.73           of Serializer (_, literals) => literals
    9.74 @@ -284,7 +283,7 @@
    9.75  
    9.76  fun mount_serializer thy alt_serializer target some_width module args naming program names =
    9.77    let
    9.78 -    val ((targets, abortable), default_width) = CodeTargetData.get thy;
    9.79 +    val ((targets, abortable), default_width) = Targets.get thy;
    9.80      fun collapse_hierarchy target =
    9.81        let
    9.82          val data = case Symtab.lookup targets target
    9.83 @@ -457,7 +456,7 @@
    9.84  fun gen_allow_abort prep_const raw_c thy =
    9.85    let
    9.86      val c = prep_const thy raw_c;
    9.87 -  in thy |> (CodeTargetData.map o apfst o apsnd) (insert (op =) c) end;
    9.88 +  in thy |> (Targets.map o apfst o apsnd) (insert (op =) c) end;
    9.89  
    9.90  
    9.91  (* concrete syntax *)
    10.1 --- a/src/Tools/Code/code_thingol.ML	Mon Jan 04 11:55:23 2010 +0100
    10.2 +++ b/src/Tools/Code/code_thingol.ML	Mon Jan 04 14:10:13 2010 +0100
    10.3 @@ -848,8 +848,8 @@
    10.4    val empty = (empty_naming, Graph.empty);
    10.5  );
    10.6  
    10.7 -fun invoke_generation thy (algebra, eqngr) f name =
    10.8 -  Program.change_yield thy (fn naming_program => (NONE, naming_program)
    10.9 +fun invoke_generation theory (algebra, eqngr) f name =
   10.10 +  Program.change_yield theory (fn thy => fn naming_program => (NONE, naming_program)
   10.11      |> f thy algebra eqngr name
   10.12      |-> (fn name => fn (_, naming_program) => (name, naming_program)));
   10.13  
    11.1 --- a/src/Tools/nbe.ML	Mon Jan 04 11:55:23 2010 +0100
    11.2 +++ b/src/Tools/nbe.ML	Mon Jan 04 14:10:13 2010 +0100
    11.3 @@ -513,15 +513,14 @@
    11.4  
    11.5  (* compilation, evaluation and reification *)
    11.6  
    11.7 -fun compile_eval thy naming program vs_t deps =
    11.8 +fun compile_eval theory naming program vs_t deps =
    11.9    let
   11.10 -    val ctxt = ProofContext.init thy;
   11.11      val (_, (gr, (_, idx_tab))) =
   11.12 -      Nbe_Functions.change thy (ensure_stmts ctxt naming program o snd);
   11.13 +      Nbe_Functions.change theory (fn thy => ensure_stmts (ProofContext.init thy) naming program o snd);
   11.14    in
   11.15      vs_t
   11.16 -    |> eval_term ctxt gr deps
   11.17 -    |> term_of_univ thy program idx_tab
   11.18 +    |> eval_term (ProofContext.init theory) gr deps
   11.19 +    |> term_of_univ theory program idx_tab
   11.20    end;
   11.21  
   11.22  (* evaluation with type reconstruction *)