--- 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 *)
--- 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 [] = []