764 end) |
764 end) |
765 | Var _ => (print_g "*** Var"; unsolvable) |
765 | Var _ => (print_g "*** Var"; unsolvable) |
766 | Bound j => (nth bounds j, accum) |
766 | Bound j => (nth bounds j, accum) |
767 | Abs (_, T, @{const False}) => (ctype_for (T --> bool_T), accum) |
767 | Abs (_, T, @{const False}) => (ctype_for (T --> bool_T), accum) |
768 | Abs (s, T, t') => |
768 | Abs (s, T, t') => |
769 let |
769 ((case t' of |
770 val C = ctype_for T |
770 t1' $ Bound 0 => |
771 val (C', accum) = do_term t' (accum |>> push_bound C) |
771 if not (loose_bvar1 (t1', 0)) then |
772 in (CFun (C, S Minus, C'), accum |>> pop_bound) end |
772 do_term (incr_boundvars ~1 t1') accum |
|
773 else |
|
774 raise SAME () |
|
775 | _ => raise SAME ()) |
|
776 handle SAME () => |
|
777 let |
|
778 val C = ctype_for T |
|
779 val (C', accum) = do_term t' (accum |>> push_bound C) |
|
780 in (CFun (C, S Minus, C'), accum |>> pop_bound) end) |
773 | Const (@{const_name All}, _) |
781 | Const (@{const_name All}, _) |
774 $ Abs (_, T', @{const "op -->"} $ (t1 $ Bound 0) $ t2) => |
782 $ Abs (_, T', @{const "op -->"} $ (t1 $ Bound 0) $ t2) => |
775 do_bounded_quantifier T' t1 t2 accum |
783 do_bounded_quantifier T' t1 t2 accum |
776 | Const (@{const_name Ex}, _) |
784 | Const (@{const_name Ex}, _) |
777 $ Abs (_, T', @{const "op &"} $ (t1 $ Bound 0) $ t2) => |
785 $ Abs (_, T', @{const "op &"} $ (t1 $ Bound 0) $ t2) => |