src/HOLCF/Tools/domain/domain_axioms.ML
changeset 29585 c23295521af5
parent 28965 1de908189869
child 30131 6be1be402ef0
child 30240 5b25fee0362c
--- a/src/HOLCF/Tools/domain/domain_axioms.ML	Wed Jan 21 16:51:45 2009 +0100
+++ b/src/HOLCF/Tools/domain/domain_axioms.ML	Wed Jan 21 18:27:43 2009 +0100
@@ -111,10 +111,10 @@
 
 fun infer_props thy = map (apsnd (FixrecPackage.legacy_infer_prop thy));
 
-fun add_axioms_i x = snd o PureThy.add_axioms (map Thm.no_attributes x);
+fun add_axioms_i x = snd o PureThy.add_axioms (map (Thm.no_attributes o apfst Binding.name) x);
 fun add_axioms_infer axms thy = add_axioms_i (infer_props thy axms) thy;
 
-fun add_defs_i x = snd o (PureThy.add_defs false) (map Thm.no_attributes x);
+fun add_defs_i x = snd o (PureThy.add_defs false) (map (Thm.no_attributes o apfst Binding.name) x);
 fun add_defs_infer defs thy = add_defs_i (infer_props thy defs) thy;
 
 in (* local *)