mk_bool_case M1 M2 b returns bool_case M1 M2 b. The prettyprinter
displays this as case b of T -> M1 || F -> M2. The bool_case constant
may be thought of as a pattern-matching version of the conditional.
FAILURE
Fails if b is not of type bool. Also fails if M1 and M2 do not
have the same type.
EXAMPLE
- mk_bool_case (Term`f x`,Term`b:'b`,Term`x:bool`);
<<HOL message: inventing new type variable names: 'a, 'b>>
> val it = `case x of T -> f x || F -> b` : term