src/HOL/Tools/recdef_package.ML
changeset 17496 26535df536ae
parent 17412 e26cb20ef0cc
child 17565 7322f37d3344
     1.1 --- a/src/HOL/Tools/recdef_package.ML	Tue Sep 20 08:20:22 2005 +0200
     1.2 +++ b/src/HOL/Tools/recdef_package.ML	Tue Sep 20 08:21:49 2005 +0200
     1.3 @@ -245,7 +245,7 @@
     1.4      val (thy, {rules = rules_idx, induct, tcs}) =
     1.5          tfl_fn strict thy cs (ss delcongs [imp_cong])
     1.6                 congs wfs name R eqs;
     1.7 -    val rules = map (map #1) (Library.partition_eq Library.eq_snd rules_idx);
     1.8 +    val rules = map (map #1) (Library.partition_eq (Library.eq_snd (op =)) rules_idx);
     1.9      val simp_att = if null tcs then
    1.10        [Simplifier.simp_add_global, RecfunCodegen.add NONE] else [];
    1.11