# HG changeset patch
# User berghofe
# Date 1098800813 -7200
# Node ID 19dcdea98649c2409ba6d2485728836c784c0362
# Parent  9237f388fbb1c02a1b83f026aeddf97a84748821
Added call to Codegen.preprocess.

diff -r 9237f388fbb1 -r 19dcdea98649 src/HOL/Tools/inductive_codegen.ML
--- a/src/HOL/Tools/inductive_codegen.ML	Tue Oct 26 16:25:41 2004 +0200
+++ b/src/HOL/Tools/inductive_codegen.ML	Tue Oct 26 16:26:53 2004 +0200
@@ -72,12 +72,12 @@
   in case Symtab.lookup (intros, s) of
       None => (case InductivePackage.get_inductive thy s of
         None => None
-      | Some ({names, ...}, {intrs, ...}) => Some (names, intrs))
+      | Some ({names, ...}, {intrs, ...}) => Some (names, preprocess thy intrs))
     | Some _ =>
         let val Some names = find_first
           (fn xs => s mem xs) (Graph.strong_conn graph)
-        in Some (names,
-          flat (map (fn s => the (Symtab.lookup (intros, s))) names))
+        in Some (names, preprocess thy
+          (flat (map (fn s => the (Symtab.lookup (intros, s))) names)))
         end
   end;
 
@@ -692,7 +692,7 @@
         None => list_of_indset thy gr dep brack t
       | Some eqns =>
           let
-            val gr' = mk_fun thy s eqns dep gr
+            val gr' = mk_fun thy s (preprocess thy eqns) dep gr
             val (gr'', ps) = foldl_map (invoke_codegen thy dep true) (gr', ts);
           in Some (gr'', mk_app brack (Pretty.str (mk_const_id
             (sign_of thy) s)) ps)
diff -r 9237f388fbb1 -r 19dcdea98649 src/HOL/Tools/recfun_codegen.ML
--- a/src/HOL/Tools/recfun_codegen.ML	Tue Oct 26 16:25:41 2004 +0200
+++ b/src/HOL/Tools/recfun_codegen.ML	Tue Oct 26 16:26:53 2004 +0200
@@ -62,8 +62,8 @@
 fun get_equations thy (s, T) =
   (case Symtab.lookup (CodegenData.get thy, s) of
      None => []
-   | Some thms => filter (fn thm => is_instance thy T
-       (snd (const_of (prop_of thm)))) thms);
+   | Some thms => preprocess thy (filter (fn thm => is_instance thy T
+       (snd (const_of (prop_of thm)))) thms));
 
 fun mk_poly_id thy (s, T) = mk_const_id (sign_of thy) s ^
   (case get_defn thy s T of
@@ -133,9 +133,10 @@
   end;
 
 fun recfun_codegen thy gr dep brack t = (case strip_comb t of
-    (Const p, ts) => (case get_equations thy p of
-       [] => None
-     | eqns =>
+    (Const (p as (s, T)), ts) => (case (get_equations thy p, get_assoc_code thy s T) of
+       ([], _) => None
+     | (_, Some _) => None
+     | (eqns, None) =>
         let val (gr', ps) = foldl_map (invoke_codegen thy dep true) (gr, ts)
         in
           Some (add_rec_funs thy gr' dep (map prop_of eqns),