src/HOL/Import/Generate-HOL/GenHOL4Base.thy
changeset 17628 f4e2587bc7a5
parent 17566 484ff733f29c
child 19233 77ca20b0ed77
--- a/src/HOL/Import/Generate-HOL/GenHOL4Base.thy	Sat Sep 24 13:54:35 2005 +0200
+++ b/src/HOL/Import/Generate-HOL/GenHOL4Base.thy	Sat Sep 24 16:43:41 2005 +0200
@@ -25,7 +25,7 @@
   COND            > HOL.If
   bool_case       > Datatype.bool.bool_case
   ONE_ONE         > HOL4Setup.ONE_ONE
-  ONTO            > HOL4Setup.ONTO
+  ONTO            > Fun.surj
   TYPE_DEFINITION > HOL4Setup.TYPE_DEFINITION
   LET             > HOL4Compat.LET;