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