src/HOLCF/Fun3.ML
changeset 9248 e1dee89de037
parent 9245 428385c4bc50
child 12030 46d57d0290a2
--- a/src/HOLCF/Fun3.ML	Wed Jul 05 14:26:58 2000 +0200
+++ b/src/HOLCF/Fun3.ML	Wed Jul 05 16:37:52 2000 +0200
@@ -5,6 +5,6 @@
 *)
 
 (* for compatibility with old HOLCF-Version *)
-val prems = goal thy "UU = (%x. UU)";
+Goal "UU = (%x. UU)";
 by (simp_tac (HOL_ss addsimps [UU_def,UU_fun_def]) 1);
 qed "inst_fun_pcpo";