--- a/src/HOLCF/Fun3.ML	Wed Mar 02 22:57:08 2005 +0100
+++ b/src/HOLCF/Fun3.ML	Wed Mar 02 23:15:16 2005 +0100
@@ -1,9 +1,4 @@
-(*  Title:      HOLCF/Fun3.ML
-    ID:         $Id$
-    Author:     Franz Regensburger
-*)
 
-(* for compatibility with old HOLCF-Version *)
-Goal "UU = (%x. UU)";
-by (simp_tac (HOL_ss addsimps [UU_def,UU_fun_def]) 1);
-qed "inst_fun_pcpo";
+(* legacy ML bindings *)
+
+val inst_fun_pcpo = thm "inst_fun_pcpo";