fixed dest atts;
authorwenzelm
Thu, 06 Dec 2001 17:16:30 +0100
changeset 12412 d0857ea70f23
parent 12411 8a8ea71c79d3
child 12413 f879fcc9412d
fixed dest atts;
src/Pure/Isar/context_rules.ML
--- 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