src/HOLCF/Cfun2.ML
changeset 4098 71e05eb27fb6
parent 3842 b55686a7b22c
child 4721 c8a8482a8124
--- a/src/HOLCF/Cfun2.ML	Mon Nov 03 12:36:48 1997 +0100
+++ b/src/HOLCF/Cfun2.ML	Mon Nov 03 14:06:27 1997 +0100
@@ -23,7 +23,7 @@
 qed_goal "less_cfun" thy "( f1 << f2 ) = (fapp(f1) << fapp(f2))"
 (fn prems =>
         [
-        (simp_tac (!simpset addsimps [inst_cfun_po]) 1)
+        (simp_tac (simpset() addsimps [inst_cfun_po]) 1)
         ]);
 
 (* ------------------------------------------------------------------------ *)