src/Pure/Isar/context_rules.ML
changeset 32784 1a5dde5079ac
parent 32091 30e2ffbba718
child 33369 470a7b233ee5
     1.1 --- a/src/Pure/Isar/context_rules.ML	Wed Sep 30 19:04:48 2009 +0200
     1.2 +++ b/src/Pure/Isar/context_rules.ML	Wed Sep 30 22:20:58 2009 +0200
     1.3 @@ -131,8 +131,8 @@
     1.4  (* retrieving rules *)
     1.5  
     1.6  fun untaglist [] = []
     1.7 -  | untaglist [(k : int * int, x)] = [x]
     1.8 -  | untaglist ((k, x) :: (rest as (k', x') :: _)) =
     1.9 +  | untaglist [(_ : int * int, x)] = [x]
    1.10 +  | untaglist ((k, x) :: (rest as (k', _) :: _)) =
    1.11        if k = k' then untaglist rest
    1.12        else x :: untaglist rest;
    1.13  
    1.14 @@ -160,7 +160,7 @@
    1.15  (* wrappers *)
    1.16  
    1.17  fun gen_add_wrapper upd w =
    1.18 -  Context.theory_map (Rules.map (fn (rs as Rules {next, rules, netpairs, wrappers}) =>
    1.19 +  Context.theory_map (Rules.map (fn Rules {next, rules, netpairs, wrappers} =>
    1.20      make_rules next rules netpairs (upd (fn ws => (w, stamp ()) :: ws) wrappers)));
    1.21  
    1.22  val addSWrapper = gen_add_wrapper Library.apfst;