src/HOL/Tools/datatype_rep_proofs.ML
changeset 8005 b64d86018785
parent 7904 2b551893583e
child 8305 93aa21ec5494
--- a/src/HOL/Tools/datatype_rep_proofs.ML	Thu Nov 11 10:24:14 1999 +0100
+++ b/src/HOL/Tools/datatype_rep_proofs.ML	Thu Nov 11 10:25:17 1999 +0100
@@ -31,7 +31,7 @@
 
 (* figure out internal names *)
 
-val image_name = Sign.intern_const (Theory.sign_of Set.thy) "op ``";
+val image_name = Sign.intern_const (Theory.sign_of Set.thy) "image";
 val UNIV_name = Sign.intern_const (Theory.sign_of Set.thy) "UNIV";
 val inj_on_name = Sign.intern_const (Theory.sign_of Fun.thy) "inj_on";
 val inv_name = Sign.intern_const (Theory.sign_of Fun.thy) "inv";