minor adaption for SML/NJ
authoroheimb
Wed Aug 12 17:40:18 1998 +0200 (1998-08-12 ago)
changeset 53076a699d5cdef4
parent 5306 3d1368a3a2a2
child 5308 3ca4da83012c
minor adaption for SML/NJ
src/FOL/simpdata.ML
src/HOL/simpdata.ML
     1.1 --- a/src/FOL/simpdata.ML	Wed Aug 12 16:49:25 1998 +0200
     1.2 +++ b/src/FOL/simpdata.ML	Wed Aug 12 17:40:18 1998 +0200
     1.3 @@ -259,8 +259,8 @@
     1.4  val split_tac        = Splitter.split_tac;
     1.5  val split_inside_tac = Splitter.split_inside_tac;
     1.6  val split_asm_tac    = Splitter.split_asm_tac;
     1.7 -val addsplits        = Splitter.addsplits;
     1.8 -val delsplits        = Splitter.delsplits;
     1.9 +val op addsplits     = Splitter.addsplits;
    1.10 +val op delsplits     = Splitter.delsplits;
    1.11  val Addsplits        = Splitter.Addsplits;
    1.12  val Delsplits        = Splitter.Delsplits;
    1.13  
     2.1 --- a/src/HOL/simpdata.ML	Wed Aug 12 16:49:25 1998 +0200
     2.2 +++ b/src/HOL/simpdata.ML	Wed Aug 12 17:40:18 1998 +0200
     2.3 @@ -344,8 +344,8 @@
     2.4  val split_tac        = Splitter.split_tac;
     2.5  val split_inside_tac = Splitter.split_inside_tac;
     2.6  val split_asm_tac    = Splitter.split_asm_tac;
     2.7 -val addsplits        = Splitter.addsplits;
     2.8 -val delsplits        = Splitter.delsplits;
     2.9 +val op addsplits     = Splitter.addsplits;
    2.10 +val op delsplits     = Splitter.delsplits;
    2.11  val Addsplits        = Splitter.Addsplits;
    2.12  val Delsplits        = Splitter.Delsplits;
    2.13