| changeset 5307 | 6a699d5cdef4 |
| parent 5304 | c133f16febc7 |
| child 5447 | df03d330aeab |
--- a/src/HOL/simpdata.ML Wed Aug 12 16:49:25 1998 +0200 +++ b/src/HOL/simpdata.ML Wed Aug 12 17:40:18 1998 +0200 @@ -344,8 +344,8 @@ val split_tac = Splitter.split_tac; val split_inside_tac = Splitter.split_inside_tac; val split_asm_tac = Splitter.split_asm_tac; -val addsplits = Splitter.addsplits; -val delsplits = Splitter.delsplits; +val op addsplits = Splitter.addsplits; +val op delsplits = Splitter.delsplits; val Addsplits = Splitter.Addsplits; val Delsplits = Splitter.Delsplits;