tuned code theorem bookkeeping

--- a/doc-src/IsarAdvanced/Codegen/Thy/Codegen.thy	Tue Jul 15 15:59:49 2008 +0200
+++ b/doc-src/IsarAdvanced/Codegen/Thy/Codegen.thy	Tue Jul 15 16:02:07 2008 +0200
@@ -501,8 +501,8 @@
 text {*
   Before selected function theorems are turned into abstract
   code, a chain of definitional transformation steps is carried
-  out: \emph{preprocessing}.  In essence, the preprocessort
-  consists of two components: a \emph{simpset} and \emph{function transformators}.
+  out: \emph{preprocessing}.  In essence, the preprocessor
+  consists of two components: a \emph{simpset} and \emph{function transformers}.
 
   The \emph{simpset} allows to employ the full generality of the Isabelle
   simplifier.  Due to the interpretation of theorems
@@ -546,22 +546,19 @@
 
 text {*
 
-  \emph{Function transformators} provide a most general interface,
+  \emph{Function transformers} provide a very general interface,
   transforming a list of function theorems to another
   list of function theorems, provided that neither the heading
   constant nor its type change.  The @{term "0\<Colon>nat"} / @{const Suc}
   pattern elimination implemented in
-  theory @{text "EfficientNat"} (\secref{eff_nat}) uses this
+  theory @{text "Efficient_Nat"} (\secref{eff_nat}) uses this
   interface.
 
   \noindent The current setup of the preprocessor may be inspected using
   the @{text "\<PRINTCODESETUP>"} command.
 
   \begin{warn}
-    Preprocessing is \emph{no} fix point process.  Keep this in mind when
-    setting up the preprocessor.
-
-    Further, the attribute \emph{code unfold}
+    The attribute \emph{code unfold}
     associated with the existing code generator also applies to
     the new one: \emph{code unfold} implies \emph{code inline}.
   \end{warn}
@@ -1096,7 +1093,7 @@
   @{index_ML Code.add_funcl: "string * thm list Susp.T -> theory -> theory"} \\
   @{index_ML Code.map_pre: "(MetaSimplifier.simpset -> MetaSimplifier.simpset) -> theory -> theory"} \\
   @{index_ML Code.map_post: "(MetaSimplifier.simpset -> MetaSimplifier.simpset) -> theory -> theory"} \\
-  @{index_ML Code.add_functrans: "string * (theory -> thm list -> thm list)
+  @{index_ML Code.add_functrans: "string * (theory -> thm list -> thm list option)
     -> theory -> theory"} \\
   @{index_ML Code.del_functrans: "string -> theory -> theory"} \\
   @{index_ML Code.add_datatype: "(string * typ) list -> theory -> theory"} \\
@@ -1120,14 +1117,16 @@
   \item @{ML Code.map_pre}~@{text "f"}~@{text "thy"} changes
      the preprocessor simpset.
 
-    \item @{ML Code.add_functrans}~@{text "(name, f)"}~@{text "thy"} adds
-     function transformator @{text f} (named @{text name}) to executable content;
-     @{text f} is a transformation of the defining equations belonging
+  \item @{ML Code.add_functrans}~@{text "(name, f)"}~@{text "thy"} adds
+     function transformer @{text f} (named @{text name}) to executable content;
+     @{text f} is a transformer of the defining equations belonging
      to a certain function definition, depending on the
-     current theory context.
+     current theory context.  Returning @{text NONE} indicates that no
+     transformation took place;  otherwise, the whole process will be iterated
+     with the new defining equations.
 
   \item @{ML Code.del_functrans}~@{text "name"}~@{text "thy"} removes
-     function transformator named @{text name} from executable content.
+     function transformer named @{text name} from executable content.
 
   \item @{ML Code.add_datatype}~@{text cs}~@{text thy} adds
      a datatype to executable content, with generation

--- a/doc-src/IsarAdvanced/Codegen/Thy/document/Codegen.tex	Tue Jul 15 15:59:49 2008 +0200
+++ b/doc-src/IsarAdvanced/Codegen/Thy/document/Codegen.tex	Tue Jul 15 16:02:07 2008 +0200
@@ -615,8 +615,8 @@
 \begin{isamarkuptext}%
 Before selected function theorems are turned into abstract
   code, a chain of definitional transformation steps is carried
-  out: \emph{preprocessing}.  In essence, the preprocessort
-  consists of two components: a \emph{simpset} and \emph{function transformators}.
+  out: \emph{preprocessing}.  In essence, the preprocessor
+  consists of two components: a \emph{simpset} and \emph{function transformers}.
 
   The \emph{simpset} allows to employ the full generality of the Isabelle
   simplifier.  Due to the interpretation of theorems
@@ -698,22 +698,19 @@
 \end{itemize}
 %
 \begin{isamarkuptext}%
-\emph{Function transformators} provide a most general interface,
+\emph{Function transformers} provide a very general interface,
   transforming a list of function theorems to another
   list of function theorems, provided that neither the heading
   constant nor its type change.  The \isa{{\isadigit{0}}} / \isa{Suc}
   pattern elimination implemented in
-  theory \isa{EfficientNat} (\secref{eff_nat}) uses this
+  theory \isa{Efficient{\isacharunderscore}Nat} (\secref{eff_nat}) uses this
   interface.
 
   \noindent The current setup of the preprocessor may be inspected using
   the \isa{{\isasymPRINTCODESETUP}} command.
 
   \begin{warn}
-    Preprocessing is \emph{no} fix point process.  Keep this in mind when
-    setting up the preprocessor.
-
-    Further, the attribute \emph{code unfold}
+    The attribute \emph{code unfold}
     associated with the existing code generator also applies to
     the new one: \emph{code unfold} implies \emph{code inline}.
   \end{warn}%
@@ -1516,7 +1513,7 @@
   \indexml{Code.add\_funcl}\verb|Code.add_funcl: string * thm list Susp.T -> theory -> theory| \\
   \indexml{Code.map\_pre}\verb|Code.map_pre: (MetaSimplifier.simpset -> MetaSimplifier.simpset) -> theory -> theory| \\
   \indexml{Code.map\_post}\verb|Code.map_post: (MetaSimplifier.simpset -> MetaSimplifier.simpset) -> theory -> theory| \\
-  \indexml{Code.add\_functrans}\verb|Code.add_functrans: string * (theory -> thm list -> thm list)|\isasep\isanewline%
+  \indexml{Code.add\_functrans}\verb|Code.add_functrans: string * (theory -> thm list -> thm list option)|\isasep\isanewline%
 \verb|    -> theory -> theory| \\
   \indexml{Code.del\_functrans}\verb|Code.del_functrans: string -> theory -> theory| \\
   \indexml{Code.add\_datatype}\verb|Code.add_datatype: (string * typ) list -> theory -> theory| \\
@@ -1541,13 +1538,15 @@
      the preprocessor simpset.
 
     \item \verb|Code.add_functrans|~\isa{{\isacharparenleft}name{\isacharcomma}\ f{\isacharparenright}}~\isa{thy} adds
-     function transformator \isa{f} (named \isa{name}) to executable content;
-     \isa{f} is a transformation of the defining equations belonging
+     function transformer \isa{f} (named \isa{name}) to executable content;
+     \isa{f} is a transformer of the defining equations belonging
      to a certain function definition, depending on the
-     current theory context.
+     current theory context.  Returning \isa{NONE} indicates that no
+     transformation took place;  otherwise, the whole process will be iterated
+     with the new defining equations.
 
   \item \verb|Code.del_functrans|~\isa{name}~\isa{thy} removes
-     function transformator named \isa{name} from executable content.
+     function transformer named \isa{name} from executable content.
 
   \item \verb|Code.add_datatype|~\isa{cs}~\isa{thy} adds
      a datatype to executable content, with generation

--- a/src/HOL/Library/Efficient_Nat.thy	Tue Jul 15 15:59:49 2008 +0200
+++ b/src/HOL/Library/Efficient_Nat.thy	Tue Jul 15 16:02:07 2008 +0200
@@ -119,8 +119,9 @@
 *}
 
 (*<*)
+setup {*
+let
 
-ML {*
 fun remove_suc thy thms =
   let
     val vname = Name.variant (map fst
@@ -159,8 +160,7 @@
               let val (ths1, ths2) = split_list thps
               in SOME (subtract Thm.eq_thm (th :: ths1) thms @ ths2) end
       end
-  in
-    case get_first mk_thms eqs of
+  in case get_first mk_thms eqs of
       NONE => thms
     | SOME x => remove_suc thy x
   end;
@@ -215,24 +215,31 @@
     then remove_suc_clause thy ths else ths
   end;
 
-fun lift_obj_eq f thy thms =
-  thms
-  |> try (
-    map (fn thm => thm RS @{thm meta_eq_to_obj_eq})
-    #> f thy
-    #> map (fn thm => thm RS @{thm eq_reflection})
-    #> map (Conv.fconv_rule Drule.beta_eta_conversion))
-  |> the_default thms
-*}
+fun lift f thy thms1 =
+  let
+    val thms2 = Drule.zero_var_indexes_list thms1;
+    val thms3 = try (map (fn thm => thm RS @{thm meta_eq_to_obj_eq})
+      #> f thy
+      #> map (fn thm => thm RS @{thm eq_reflection})
+      #> map (Conv.fconv_rule Drule.beta_eta_conversion)) thms2;
+    val thms4 = Option.map Drule.zero_var_indexes_list thms3;
+  in case thms4
+   of NONE => NONE
+    | SOME thms4 => if Thm.eq_thms (thms2, thms4) then NONE else SOME thms4
+  end
 
-setup {*
+in
+
   Codegen.add_preprocessor eqn_suc_preproc
   #> Codegen.add_preprocessor clause_suc_preproc
-  #> Code.add_functrans ("eqn_Suc", lift_obj_eq eqn_suc_preproc)
-  #> Code.add_functrans ("clause_Suc", lift_obj_eq clause_suc_preproc)
+  #> Code.add_functrans ("eqn_Suc", lift eqn_suc_preproc)
+  #> Code.add_functrans ("clause_Suc", lift clause_suc_preproc)
+
+end;
 *}
 (*>*)
 
+
 subsection {* Target language setup *}
 
 text {*

--- a/src/Pure/Isar/code.ML	Tue Jul 15 15:59:49 2008 +0200
+++ b/src/Pure/Isar/code.ML	Tue Jul 15 16:02:07 2008 +0200
@@ -21,7 +21,7 @@
   val del_inline: thm -> theory -> theory
   val add_post: thm -> theory -> theory
   val del_post: thm -> theory -> theory
-  val add_functrans: string * (theory -> thm list -> thm list) -> theory -> theory
+  val add_functrans: string * (theory -> thm list -> thm list option) -> theory -> theory
   val del_functrans: string -> theory -> theory
   val add_datatype: (string * typ) list -> theory -> theory
   val add_datatype_cmd: string list -> theory -> theory
@@ -54,8 +54,7 @@
 sig
   type T
   val empty: T
-  val merge: Pretty.pp -> T * T -> T
-  val purge: theory option -> string list option -> T -> T
+  val purge: theory -> string list -> T -> T
 end;
 
 signature CODE_DATA =
@@ -69,8 +68,8 @@
 signature PRIVATE_CODE =
 sig
   include CODE
-  val declare_data: Object.T -> (Pretty.pp -> Object.T * Object.T -> Object.T)
-    -> (theory option -> string list option -> Object.T -> Object.T) -> serial
+  val declare_data: Object.T -> (theory -> string list -> Object.T -> Object.T)
+    -> serial
   val get_data: serial * ('a -> Object.T) * (Object.T -> 'a)
     -> theory -> 'a
   val change_data: serial * ('a -> Object.T) * (Object.T -> 'a)
@@ -171,10 +170,6 @@
 
 fun pretty_sdthms ctxt (sels, _) = pretty_lthms ctxt sels;
 
-
-(* fundamental melting operations *)
-(*FIXME delete*)
-
 fun melt _ ([], []) = (false, [])
   | melt _ ([], ys) = (true, ys)
   | melt eq (xs, ys) = fold_rev
@@ -200,17 +195,15 @@
         (subtract Thm.eq_thm_prop dels2 (Susp.force sels1), Susp.force sels2);
       val (_, dels) = melt_thms
         (subtract Thm.eq_thm_prop (Susp.force sels2) dels1, dels2);
-    in (true, ((Susp.delay o K) sels, dels)) end
+    in ((Susp.delay o K) sels, dels) end
     else let
-      val (sels_t, sels) = melt_lthms (sels1, sels2);
-    in (sels_t, (sels, dels)) end
+      val (_, sels) = melt_lthms (sels1, sels2);
+    in (sels, dels) end
   end;
 
 
 (* specification data *)
 
-val merge_funcs = Symtab.join (fn _ => fn ((_, a), (_, b)) => melt_sdthms (a, b));
-
 val eq_string = op = : string * string -> bool;
 fun eq_dtyp ((vs1, cs1), (vs2, cs2)) = 
   gen_eq_set (eq_pair eq_string (gen_eq_set eq_string)) (vs1, vs2)
@@ -220,11 +213,8 @@
     fun join _ (cos as (_, cos2)) = if eq_dtyp cos then raise Symtab.SAME else cos2;
   in Symtab.join join tabs end;
 
-fun merge_cases ((cases1, undefs1), (cases2, undefs2)) =
-  (Symtab.merge (K true) (cases1, cases2), Symtab.merge (K true) (undefs1, undefs2));
-
 datatype spec = Spec of {
-  funcs: (bool * sdthms) Symtab.table,
+  funcs: sdthms Symtab.table,
   dtyps: ((string * sort) list * (string * typ list) list) Symtab.table,
   cases: (int * string list) Symtab.table * unit Symtab.table
 };
@@ -233,12 +223,13 @@
   Spec { funcs = funcs, dtyps = dtyps, cases = cases };
 fun map_spec f (Spec { funcs = funcs, dtyps = dtyps, cases = cases }) =
   mk_spec (f (funcs, (dtyps, cases)));
-fun merge_spec (Spec { funcs = funcs1, dtyps = dtyps1, cases = cases1 },
-  Spec { funcs = funcs2, dtyps = dtyps2, cases = cases2 }) =
+fun merge_spec (Spec { funcs = funcs1, dtyps = dtyps1, cases = (cases1, undefs1) },
+  Spec { funcs = funcs2, dtyps = dtyps2, cases = (cases2, undefs2) }) =
   let
-    val funcs = merge_funcs (funcs1, funcs2);
+    val funcs = Symtab.join (K melt_sdthms) (funcs1, funcs2);
     val dtyps = merge_dtyps (dtyps1, dtyps2);
-    val cases = merge_cases (cases1, cases2);
+    val cases = (Symtab.merge (K true) (cases1, cases2),
+      Symtab.merge (K true) (undefs1, undefs2));
   in mk_spec (funcs, (dtyps, cases)) end;
 
 
@@ -247,7 +238,7 @@
 datatype thmproc = Thmproc of {
   pre: MetaSimplifier.simpset,
   post: MetaSimplifier.simpset,
-  functrans: (string * (serial * (theory -> thm list -> thm list))) list
+  functrans: (string * (serial * (theory -> thm list -> thm list option))) list
 };
 
 fun mk_thmproc ((pre, post), functrans) =
@@ -300,8 +291,7 @@
 
 type kind = {
   empty: Object.T,
-  merge: Pretty.pp -> Object.T * Object.T -> Object.T,
-  purge: theory option -> string list option -> Object.T -> Object.T
+  purge: theory -> string list -> Object.T -> Object.T
 };
 
 val kinds = ref (Datatab.empty: kind Datatab.table);
@@ -313,22 +303,19 @@
 
 in
 
-fun declare_data empty merge purge =
+fun declare_data empty purge =
   let
     val k = serial ();
-    val kind = {empty = empty, merge = merge, purge = purge};
+    val kind = {empty = empty, purge = purge};
     val _ = change kinds (Datatab.update (k, kind));
     val _ = change kind_keys (cons k);
   in k end;
 
-fun invoke_empty k = invoke (fn kind => #empty kind) k;
+fun invoke_init k = invoke (fn kind => #empty kind) k;
 
-fun invoke_merge_all pp = Datatab.join
-  (invoke (fn kind => #merge kind pp));
-
-fun invoke_purge_all thy_opt cs =
+fun invoke_purge_all thy cs =
   fold (fn k => Datatab.map_entry k
-    (invoke (fn kind => #purge kind thy_opt cs) k)) (! kind_keys);
+    (invoke (fn kind => #purge kind thy cs) k)) (! kind_keys);
 
 end; (*local*)
 
@@ -338,20 +325,16 @@
 local
 
 type data = Object.T Datatab.table;
+val empty_data = Datatab.empty : data;
 
 structure CodeData = TheoryDataFun
 (
   type T = exec * data ref;
-  val empty = (empty_exec, ref Datatab.empty : data ref);
+  val empty = (empty_exec, ref empty_data);
   fun copy (exec, data) = (exec, ref (! data));
   val extend = copy;
   fun merge pp ((exec1, data1), (exec2, data2)) =
-    let
-      val exec = merge_exec (exec1, exec2);
-      val data1' = invoke_purge_all NONE NONE (! data1);
-      val data2' = invoke_purge_all NONE NONE (! data2);
-      val data = invoke_merge_all pp (data1', data2');
-    in (exec, ref data) end;
+    (merge_exec (exec1, exec2), ref empty_data);
 );
 
 val _ = Context.>> (Context.map_theory CodeData.init);
@@ -361,7 +344,7 @@
 fun get_ensure_init kind data_ref =
   case Datatab.lookup (! data_ref) kind
    of SOME x => x
-    | NONE => let val y = invoke_empty kind
+    | NONE => let val y = invoke_init kind
         in (change data_ref (Datatab.update (kind, y)); y) end;
 
 in
@@ -371,8 +354,9 @@
 val the_exec = fst o CodeData.get;
 
 fun map_exec_purge touched f thy =
-  CodeData.map (fn (exec, data) => 
-    (f exec, ref (invoke_purge_all (SOME thy) touched (! data)))) thy;
+  CodeData.map (fn (exec, data) => (f exec, ref (case touched
+   of SOME cs => invoke_purge_all thy cs (! data)
+    | NONE => empty_data))) thy;
 
 
 (* access to data dependent on abstract executable content *)
@@ -426,9 +410,8 @@
     val pre = (#pre o the_thmproc) exec;
     val post = (#post o the_thmproc) exec;
     val functrans = (map fst o #functrans o the_thmproc) exec;
-    val funs = the_funcs exec
+    val funcs = the_funcs exec
       |> Symtab.dest
-      |> (map o apsnd) snd
       |> (map o apfst) (CodeUnit.string_of_const thy)
       |> sort (string_ord o pairself fst);
     val dtyps = the_dtyps exec
@@ -441,7 +424,7 @@
       Pretty.block (
         Pretty.str "defining equations:"
         :: Pretty.fbrk
-        :: (Pretty.fbreaks o map pretty_func) funs
+        :: (Pretty.fbreaks o map pretty_func) funcs
       ),
       Pretty.block [
         Pretty.str "preprocessing simpset:",
@@ -454,7 +437,7 @@
         MetaSimplifier.pretty_ss post
       ],
       Pretty.block (
-        Pretty.str "function transformators:"
+        Pretty.str "function transformers:"
         :: Pretty.fbrk
         :: (Pretty.fbreaks o map Pretty.str) functrans
       ),
@@ -527,7 +510,7 @@
     val funcs = classparams
       |> map_filter (fn c => try (AxClass.param_of_inst thy) (c, tyco))
       |> map (Symtab.lookup ((the_funcs o the_exec) thy))
-      |> (map o Option.map) (Susp.force o fst o snd)
+      |> (map o Option.map) (Susp.force o fst)
       |> maps these
       |> map (Thm.transfer thy)
     fun sorts_of [Type (_, tys)] = map (snd o dest_TVar) tys
@@ -704,7 +687,7 @@
       else ();
   in
     (map_exec_purge (SOME [c]) o map_funcs) (Symtab.map_default
-      (c, (false, (Susp.value [], []))) (apsnd (add_thm func))) thy
+      (c, (Susp.value [], [])) (add_thm func)) thy
   end;
 
 fun add_liberal_func thm thy =
@@ -716,7 +699,7 @@
           then thy
           else map_exec_purge (SOME [c]) (map_funcs
             (Symtab.map_default
-              (c, (false, (Susp.value [], []))) (apsnd (add_thm func)))) thy
+              (c, (Susp.value [], [])) (add_thm func))) thy
         end
     | NONE => thy;
 
@@ -729,7 +712,7 @@
           then thy
           else map_exec_purge (SOME [c]) (map_funcs
           (Symtab.map_default
-            (c, (false, (Susp.value [], []))) (apsnd (add_thm func)))) thy
+            (c, (Susp.value [], [])) (add_thm func))) thy
         end
     | NONE => thy;
 
@@ -738,12 +721,12 @@
    of SOME func => let
           val c = const_of_func thy func;
         in map_exec_purge (SOME [c]) (map_funcs
-          (Symtab.map_entry c (apsnd (del_thm func)))) thy
+          (Symtab.map_entry c (del_thm func))) thy
         end
     | NONE => thy;
 
 fun del_funcs const = map_exec_purge (SOME [const])
-  (map_funcs (Symtab.map_entry const (apsnd del_thms)));
+  (map_funcs (Symtab.map_entry const del_thms));
 
 fun add_funcl (const, lthms) thy =
   let
@@ -752,8 +735,8 @@
         alas, naive checking results in non-termination!*)
   in
     map_exec_purge (SOME [const])
-      (map_funcs (Symtab.map_default (const, (false, (Susp.value [], [])))
-      (apsnd (add_lthms lthms')))) thy
+      (map_funcs (Symtab.map_default (const, (Susp.value [], []))
+      (add_lthms lthms'))) thy
   end;
 
 val add_default_func_attr = Attrib.internal (fn _ => Thm.declaration_attribute
@@ -819,7 +802,7 @@
 
 fun del_functrans name =
   (map_exec_purge NONE o map_thmproc o apsnd)
-    (delete_force "function transformator" name);
+    (delete_force "function transformer" name);
 
 val _ = Context.>> (Context.map_theory
   (let
@@ -841,11 +824,13 @@
 
 local
 
-fun apply_functrans thy f [] = []
-  | apply_functrans thy f (thms as (thm :: _)) =
+fun apply_functrans thy [] = []
+  | apply_functrans thy (thms as thm :: _) =
       let
         val const = const_of_func thy thm;
-        val thms' = f thy thms;
+        val functrans = (map (fn (_, (_, f)) => f thy) o #functrans
+          o the_thmproc o the_exec) thy;
+        val thms' = perhaps (perhaps_loop (perhaps_apply functrans)) thms;
       in certify_const thy const thms' end;
 
 fun rhs_conv conv thm =
@@ -867,7 +852,7 @@
     val pre = (Simplifier.theory_context thy o #pre o the_thmproc o the_exec) thy;
   in
     thms
-    |> fold (fn (_, (_, f)) => apply_functrans thy f) ((#functrans o the_thmproc o the_exec) thy)
+    |> apply_functrans thy
     |> map (CodeUnit.rewrite_func pre)
     (*FIXME - must check gere: rewrite rule, defining equation, proper constant *)
     |> map (AxClass.unoverload thy)
@@ -913,7 +898,7 @@
 
 fun get_funcs thy const =
   Symtab.lookup ((the_funcs o the_exec) thy) const
-  |> Option.map (Susp.force o fst o snd)
+  |> Option.map (Susp.force o fst)
   |> these
   |> map (Thm.transfer thy);
 
@@ -950,8 +935,7 @@
 fun dest (Data x) = x
 
 val kind = Code.declare_data (Data Data.empty)
-  (fn pp => fn (Data x1, Data x2) => Data (Data.merge pp (x1, x2)))
-  (fn thy_opt => fn cs => fn Data x => Data (Data.purge thy_opt cs x));
+  (fn thy => fn cs => fn Data x => Data (Data.purge thy cs x));
 
 val data_op = (kind, Data, dest);
 

--- a/src/Tools/code/code_funcgr.ML	Tue Jul 15 15:59:49 2008 +0200
+++ b/src/Tools/code/code_funcgr.ML	Tue Jul 15 16:02:07 2008 +0200
@@ -261,11 +261,9 @@
 (
   type T = T;
   val empty = Graph.empty;
-  fun merge _ _ = Graph.empty;
-  fun purge _ NONE _ = Graph.empty
-    | purge _ (SOME cs) funcgr =
-        Graph.del_nodes ((Graph.all_preds funcgr 
-          o filter (can (Graph.get_node funcgr))) cs) funcgr;
+  fun purge _ cs funcgr =
+    Graph.del_nodes ((Graph.all_preds funcgr 
+      o filter (can (Graph.get_node funcgr))) cs) funcgr;
 );
 
 fun make thy =

--- a/src/Tools/code/code_name.ML	Tue Jul 15 15:59:49 2008 +0200
+++ b/src/Tools/code/code_name.ML	Tue Jul 15 16:02:07 2008 +0200
@@ -303,12 +303,8 @@
 (
   type T = const Symtab.table * string Symtab.table;
   val empty = (Symtab.empty, Symtab.empty);
-  fun merge _ ((const1, constrev1), (const2, constrev2)) : T =
-    (Symtab.merge (op =) (const1, const2),
-      Symtab.merge (op =) (constrev1, constrev2));
-  fun purge _ NONE _ = empty
-    | purge _ (SOME cs) (const, constrev) = (fold Symtab.delete_safe cs const,
-        fold Symtab.delete_safe (map_filter (Symtab.lookup const) cs) constrev);
+  fun purge _ cs (const, constrev) = (fold Symtab.delete_safe cs const,
+    fold Symtab.delete_safe (map_filter (Symtab.lookup const) cs) constrev);
 );
 
 val setup = CodeName.init;

--- a/src/Tools/code/code_thingol.ML	Tue Jul 15 15:59:49 2008 +0200
+++ b/src/Tools/code/code_thingol.ML	Tue Jul 15 16:02:07 2008 +0200
@@ -569,18 +569,15 @@
 (
   type T = program;
   val empty = Graph.empty;
-  fun merge _ = Graph.merge (K true);
-  fun purge _ NONE _ = Graph.empty
-    | purge NONE _ _ = Graph.empty
-    | purge (SOME thy) (SOME cs) program =
-        let
-          val cs_exisiting =
-            map_filter (CodeName.const_rev thy) (Graph.keys program);
-          val dels = (Graph.all_preds program
-              o map (CodeName.const thy)
-              o filter (member (op =) cs_exisiting)
-            ) cs;
-        in Graph.del_nodes dels program end;
+  fun purge thy cs program =
+    let
+      val cs_exisiting =
+        map_filter (CodeName.const_rev thy) (Graph.keys program);
+      val dels = (Graph.all_preds program
+          o map (CodeName.const thy)
+          o filter (member (op =) cs_exisiting)
+        ) cs;
+    in Graph.del_nodes dels program end;
 );
 
 val cached_program = Program.get;

--- a/src/Tools/nbe.ML	Tue Jul 15 15:59:49 2008 +0200
+++ b/src/Tools/nbe.ML	Tue Jul 15 16:02:07 2008 +0200
@@ -346,20 +346,15 @@
 (
   type T = (Univ option * int) Graph.T * (int * string Inttab.table);
   val empty = (Graph.empty, (0, Inttab.empty));
-  fun merge _ ((gr1, (maxidx1, idx_tab1)), (gr2, (maxidx2, idx_tab2))) =
-    (Graph.merge (K true) (gr1, gr2), (IntInf.max (maxidx1, maxidx2),
-      Inttab.merge (K true) (idx_tab1, idx_tab2)));
-  fun purge _ NONE _ = empty
-    | purge NONE _ _ = empty
-    | purge (SOME thy) (SOME cs) (gr, (maxidx, idx_tab)) =
-        let
-          val cs_exisiting =
-            map_filter (CodeName.const_rev thy) (Graph.keys gr);
-          val dels = (Graph.all_preds gr
-              o map (CodeName.const thy)
-              o filter (member (op =) cs_exisiting)
-            ) cs;
-        in (Graph.del_nodes dels gr, (maxidx, idx_tab)) end;
+  fun purge thy cs (gr, (maxidx, idx_tab)) =
+    let
+      val cs_exisiting =
+        map_filter (CodeName.const_rev thy) (Graph.keys gr);
+      val dels = (Graph.all_preds gr
+          o map (CodeName.const thy)
+          o filter (member (op =) cs_exisiting)
+        ) cs;
+    in (Graph.del_nodes dels gr, (maxidx, idx_tab)) end;
 );
 
 (* compilation, evaluation and reification *)