src/Pure/Isar/constdefs.ML
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;