changeset 22796 | 34c316d7b630 |
parent 22761 | c2e9705f804e |
child 24219 | e558fe311376 |
--- a/src/Pure/Isar/constdefs.ML Thu Apr 26 12:00:01 2007 +0200 +++ b/src/Pure/Isar/constdefs.ML Thu Apr 26 12:00:05 2007 +0200 @@ -49,7 +49,7 @@ val thy' = thy - |> Theory.add_consts_i [(c, T, mx)] + |> Sign.add_consts_i [(c, T, mx)] |> PureThy.add_defs_i false [((name, def), atts)] |-> (fn [thm] => CodegenData.add_func false thm); in ((c, T), thy') end;