src/Pure/Isar/context_rules.ML

 
 fun del map_data (x, th) =
   (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
 
 val intro_bang_global  = add intro_bangK I GlobalRules.map;
 val elim_bang_global   = add elim_bangK I GlobalRules.map;