src/Pure/Isar/context_rules.ML
changeset 17496 26535df536ae
parent 17351 f7f2f56fcc28
child 17511 51314f4bd01d
     1.1 --- a/src/Pure/Isar/context_rules.ML	Tue Sep 20 08:20:22 2005 +0200
     1.2 +++ b/src/Pure/Isar/context_rules.ML	Tue Sep 20 08:21:49 2005 +0200
     1.3 @@ -131,7 +131,7 @@
     1.4    fun merge _ (Rules {rules = rules1, wrappers = (ws1, ws1'), ...},
     1.5        Rules {rules = rules2, wrappers = (ws2, ws2'), ...}) =
     1.6      let
     1.7 -      val wrappers = (gen_merge_lists' eq_snd ws1 ws2, gen_merge_lists' eq_snd ws1' ws2');
     1.8 +      val wrappers = (gen_merge_lists' (eq_snd (op =)) ws1 ws2, gen_merge_lists' (eq_snd (op =)) ws1' ws2');
     1.9        val rules = gen_merge_lists' (fn ((_, (k1, th1)), (_, (k2, th2))) =>
    1.10            k1 = k2 andalso Drule.eq_thm_prop (th1, th2)) rules1 rules2;
    1.11        val next = ~ (length rules);