changeset 67399 | eab6ce8368fa |
parent 66251 | cd935b7cb3fb |
child 67405 | e9ab4ad7bd15 |
--- a/src/HOL/Tools/Ctr_Sugar/ctr_sugar.ML Wed Jan 10 15:21:49 2018 +0100 +++ b/src/HOL/Tools/Ctr_Sugar/ctr_sugar.ML Wed Jan 10 15:25:09 2018 +0100 @@ -477,7 +477,7 @@ ||>> 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);