# HG changeset patch # User haftmann # Date 1177084707 -7200 # Node ID c2e9705f804ec67eb1bbe5ba4a1a2c97d3b558ef # Parent 6eafeffe801c6f3836e9c0a020e5d0aa67bbb27a defs are added to code data diff -r 6eafeffe801c -r c2e9705f804e src/Pure/Isar/constdefs.ML --- a/src/Pure/Isar/constdefs.ML Fri Apr 20 17:58:26 2007 +0200 +++ b/src/Pure/Isar/constdefs.ML Fri Apr 20 17:58:27 2007 +0200 @@ -50,7 +50,8 @@ val thy' = thy |> Theory.add_consts_i [(c, T, mx)] - |> PureThy.add_defs_i false [((name, def), atts)] |> snd; + |> PureThy.add_defs_i false [((name, def), atts)] + |-> (fn [thm] => CodegenData.add_func false thm); in ((c, T), thy') end; fun gen_constdefs prep_vars prep_prop prep_att (raw_structs, specs) thy =