src/HOL/Tools/Ctr_Sugar/ctr_sugar.ML

       ||>> mk_Freess "x" ctr_Tss
       ||>> mk_Freess "y" ctr_Tss
       ||>> mk_Frees "f" case_Ts
       ||>> mk_Frees "g" case_Ts
       ||>> yield_singleton (mk_Frees "z") B
-      ||>> yield_singleton (apfst (op ~~) oo mk_Frees' "P") HOLogic.boolT;
+      ||>> yield_singleton (apfst (~~) oo mk_Frees' "P") HOLogic.boolT;
 
     val q = Free (fst p', mk_pred1T B);
 
     val xctrs = map2 (curry Term.list_comb) ctrs xss;
     val yctrs = map2 (curry Term.list_comb) ctrs yss;