src/HOLCF/Fun3.ML
changeset 3842 b55686a7b22c
parent 2640 ee4dfce170a0
child 9245 428385c4bc50
--- a/src/HOLCF/Fun3.ML	Fri Oct 10 18:37:49 1997 +0200
+++ b/src/HOLCF/Fun3.ML	Fri Oct 10 19:02:28 1997 +0200
@@ -7,7 +7,7 @@
 open Fun3;
 
 (* for compatibility with old HOLCF-Version *)
-qed_goal "inst_fun_pcpo" thy "UU = (%x.UU)"
+qed_goal "inst_fun_pcpo" thy "UU = (%x. UU)"
  (fn prems => 
         [
         (simp_tac (HOL_ss addsimps [UU_def,UU_fun_def]) 1)