src/HOLCF/Fun3.ML

--- a/src/HOLCF/Fun3.ML	Sat Feb 15 18:24:05 1997 +0100
+++ b/src/HOLCF/Fun3.ML	Mon Feb 17 10:57:11 1997 +0100
@@ -5,3 +5,10 @@
 *)
 
 open Fun3;
+
+(* for compatibility with old HOLCF-Version *)
+qed_goal "inst_fun_pcpo" thy "UU = (%x.UU)"
+ (fn prems => 
+        [
+        (simp_tac (HOL_ss addsimps [UU_def,UU_fun_def]) 1)
+        ]);