diff -r 8a8ea71c79d3 -r d0857ea70f23 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