--- 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;