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) ]); (* ------------------------------------------------------------------------ *)