--- a/src/HOLCF/domain/axioms.ML Tue Dec 06 06:22:14 2005 +0100
+++ b/src/HOLCF/domain/axioms.ML Tue Dec 06 09:04:09 2005 +0100
@@ -114,7 +114,7 @@
fun add_axioms_i x = #1 o PureThy.add_axioms_i (map Thm.no_attributes x);
fun add_axioms_infer axms thy = add_axioms_i (infer_types thy axms) thy;
-fun add_defs_i x = #1 o (PureThy.add_defs_i false) (map Thm.no_attributes x);
+fun add_defs_i x = snd o (PureThy.add_defs_i false) (map Thm.no_attributes x);
fun add_defs_infer defs thy = add_defs_i (infer_types thy defs) thy;
in (* local *)