# HG changeset patch
# User haftmann
# Date 1237386232 -3600
# Node ID 8fac7efcce0ad12502d6dd27dfcc452816e44626
# Parent  696f93184f0d3ee01b8f48a54f879d2b6ee7cb7a
made SML/NJ happy

diff -r 696f93184f0d -r 8fac7efcce0a src/Provers/splitter.ML
--- a/src/Provers/splitter.ML	Wed Mar 18 11:57:28 2009 +0100
+++ b/src/Provers/splitter.ML	Wed Mar 18 15:23:52 2009 +0100
@@ -472,8 +472,8 @@
   Args.$$$ splitN -- Args.add -- Args.colon >> K (I, split_add),
   Args.$$$ splitN -- Args.del -- Args.colon >> K (I, split_del)];
 
-val split_meth = Attrib.thms >>
-  (fn ths => K (SIMPLE_METHOD' (CHANGED_PROP o gen_split_tac ths)));
+fun split_meth parser = (Attrib.thms >>
+  (fn ths => K (SIMPLE_METHOD' (CHANGED_PROP o gen_split_tac ths)))) parser;
 
 
 (* theory setup *)
diff -r 696f93184f0d -r 8fac7efcce0a src/Pure/library.ML
--- a/src/Pure/library.ML	Wed Mar 18 11:57:28 2009 +0100
+++ b/src/Pure/library.ML	Wed Mar 18 15:23:52 2009 +0100
@@ -1022,7 +1022,7 @@
 
 (*insert tags*)
 fun tag_list k [] = []
-  | tag_list k (x :: xs) = (k, x) :: tag_list (k + 1) xs;
+  | tag_list k (x :: xs) = (k:int, x) :: tag_list (k + 1) xs;
 
 (*remove tags and suppress duplicates -- list is assumed sorted!*)
 fun untag_list [] = []