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