--- a/src/HOL/Fun.thy Thu Oct 29 08:14:39 2009 +0100
+++ b/src/HOL/Fun.thy Thu Oct 29 11:41:36 2009 +0100
@@ -7,7 +7,6 @@
theory Fun
imports Complete_Lattice
-uses ("Tools/transfer.ML")
begin
text{*As a simplification rule, it replaces all function equalities by
@@ -604,16 +603,6 @@
*}
-subsection {* Generic transfer procedure *}
-
-definition TransferMorphism:: "('b \<Rightarrow> 'a) \<Rightarrow> 'b set \<Rightarrow> bool"
- where "TransferMorphism a B \<longleftrightarrow> True"
-
-use "Tools/transfer.ML"
-
-setup Transfer.setup
-
-
subsection {* Code generator setup *}
types_code