src/Pure/Isar/context_rules.ML
changeset 12412 d0857ea70f23
parent 12399 2ba27248af7f
child 12805 3be853cf19cf
     1.1 --- a/src/Pure/Isar/context_rules.ML	Thu Dec 06 17:16:16 2001 +0100
     1.2 +++ b/src/Pure/Isar/context_rules.ML	Thu Dec 06 17:16:30 2001 +0100
     1.3 @@ -219,7 +219,7 @@
     1.4    (map_data (del_rule th o del_rule (Tactic.make_elim th)) x, th);
     1.5  
     1.6  fun add k view map_data opt_w =
     1.7 -  (fn (x, th) => (map_data (add_rule k opt_w th) x, th)) o del map_data;
     1.8 +  (fn (x, th) => (map_data (add_rule k opt_w (view th)) x, th)) o del map_data;
     1.9  
    1.10  in
    1.11