diff -r e43d761a742d -r 1a5dde5079ac src/Pure/Isar/context_rules.ML
--- a/src/Pure/Isar/context_rules.ML	Wed Sep 30 19:04:48 2009 +0200
+++ b/src/Pure/Isar/context_rules.ML	Wed Sep 30 22:20:58 2009 +0200
@@ -131,8 +131,8 @@
 (* retrieving rules *)
 
 fun untaglist [] = []
-  | untaglist [(k : int * int, x)] = [x]
-  | untaglist ((k, x) :: (rest as (k', x') :: _)) =
+  | untaglist [(_ : int * int, x)] = [x]
+  | untaglist ((k, x) :: (rest as (k', _) :: _)) =
       if k = k' then untaglist rest
       else x :: untaglist rest;
 
@@ -160,7 +160,7 @@
 (* wrappers *)
 
 fun gen_add_wrapper upd w =
-  Context.theory_map (Rules.map (fn (rs as Rules {next, rules, netpairs, wrappers}) =>
+  Context.theory_map (Rules.map (fn Rules {next, rules, netpairs, wrappers} =>
     make_rules next rules netpairs (upd (fn ws => (w, stamp ()) :: ws) wrappers)));
 
 val addSWrapper = gen_add_wrapper Library.apfst;