src/HOLCF/cont_consts.ML
changeset 22796 34c316d7b630
parent 22675 acf10be7dcca
--- a/src/HOLCF/cont_consts.ML	Thu Apr 26 12:00:01 2007 +0200
+++ b/src/HOLCF/cont_consts.ML	Thu Apr 26 12:00:05 2007 +0200
@@ -85,10 +85,10 @@
     val transformed_decls = map transform contconst_decls;
   in
     thy
-    |> Theory.add_consts_i normal_decls
-    |> Theory.add_consts_i (map first transformed_decls)
-    |> Theory.add_syntax_i (map second transformed_decls)
-    |> Theory.add_trrules_i (List.concat (map third transformed_decls))
+    |> Sign.add_consts_i normal_decls
+    |> Sign.add_consts_i (map first transformed_decls)
+    |> Sign.add_syntax_i (map second transformed_decls)
+    |> Sign.add_trrules_i (List.concat (map third transformed_decls))
   end;
 
 val add_consts = gen_add_consts Sign.read_typ;