# HG changeset patch
# User oheimb
# Date 902936418 -7200
# Node ID 6a699d5cdef459ac29d099ce6e6c97270e7bc562
# Parent  3d1368a3a2a275c460d23bcbd247ee8d5bbb9f35
minor adaption for SML/NJ

diff -r 3d1368a3a2a2 -r 6a699d5cdef4 src/FOL/simpdata.ML
--- a/src/FOL/simpdata.ML	Wed Aug 12 16:49:25 1998 +0200
+++ b/src/FOL/simpdata.ML	Wed Aug 12 17:40:18 1998 +0200
@@ -259,8 +259,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;
 
diff -r 3d1368a3a2a2 -r 6a699d5cdef4 src/HOL/simpdata.ML
--- 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;