| changeset 4091 | 771b1f6422a8 |
| parent 3859 | 810fccb1ebe4 |
| child 5137 | 60205b0de9b9 |
--- a/src/ZF/simpdata.ML Mon Nov 03 12:22:43 1997 +0100 +++ b/src/ZF/simpdata.ML Mon Nov 03 12:24:13 1997 +0100 @@ -104,6 +104,6 @@ val ZF_atomize = atomize (ZF_conn_pairs, ZF_mem_pairs); -simpset := !simpset setmksimps (map mk_meta_eq o ZF_atomize o gen_all); +simpset_ref() := simpset() setmksimps (map mk_meta_eq o ZF_atomize o gen_all); -val ZF_ss = !simpset; +val ZF_ss = simpset();