src/HOLCF/Cont.ML
changeset 4098 71e05eb27fb6
parent 3842 b55686a7b22c
child 4721 c8a8482a8124
--- a/src/HOLCF/Cont.ML	Mon Nov 03 12:36:48 1997 +0100
+++ b/src/HOLCF/Cont.ML	Mon Nov 03 14:06:27 1997 +0100
@@ -666,7 +666,7 @@
 	cut_facts_tac prems 1,
 	strip_tac 1,
 	dtac (ax_flat RS spec RS spec RS mp) 1,
-	fast_tac ((HOL_cs addss (!simpset addsimps [minimal]))) 1
+	fast_tac ((HOL_cs addss (simpset() addsimps [minimal]))) 1
 	]);