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)