566 | mark Ts (t as Const ("_bound", _) $ u) = if is_prop Ts u then aprop t else t |
566 | mark Ts (t as Const ("_bound", _) $ u) = if is_prop Ts u then aprop t else t |
567 | mark Ts (t as Free _) = if is_prop Ts t then aprop t else t |
567 | mark Ts (t as Free _) = if is_prop Ts t then aprop t else t |
568 | mark Ts (t as Var _) = if is_prop Ts t then aprop t else t |
568 | mark Ts (t as Var _) = if is_prop Ts t then aprop t else t |
569 | mark Ts (t as Bound _) = if is_prop Ts t then aprop t else t |
569 | mark Ts (t as Bound _) = if is_prop Ts t then aprop t else t |
570 | mark Ts (Abs (x, T, t)) = Abs (x, T, mark (T :: Ts) t) |
570 | mark Ts (Abs (x, T, t)) = Abs (x, T, mark (T :: Ts) t) |
571 | mark Ts (t as t1 $ (t2 as Const ("TYPE", Type ("itself", [T])))) = |
571 | mark Ts (t as t1 $ (t2 as Const ("Pure.type", Type ("itself", [T])))) = |
572 if is_prop Ts t andalso not (is_term t) then Const ("_type_prop", T) $ mark Ts t1 |
572 if is_prop Ts t andalso not (is_term t) then Const ("_type_prop", T) $ mark Ts t1 |
573 else mark Ts t1 $ mark Ts t2 |
573 else mark Ts t1 $ mark Ts t2 |
574 | mark Ts (t as t1 $ t2) = |
574 | mark Ts (t as t1 $ t2) = |
575 (if is_Const (Term.head_of t) orelse not (is_prop Ts t) then I else aprop) |
575 (if is_Const (Term.head_of t) orelse not (is_prop Ts t) then I else aprop) |
576 (mark Ts t1 $ mark Ts t2); |
576 (mark Ts t1 $ mark Ts t2); |
832 (Sign.parse_ast_translation |
832 (Sign.parse_ast_translation |
833 [("_context_const", const_ast_tr true), |
833 [("_context_const", const_ast_tr true), |
834 ("_context_xconst", const_ast_tr false)] #> |
834 ("_context_xconst", const_ast_tr false)] #> |
835 Sign.typed_print_translation |
835 Sign.typed_print_translation |
836 [("_type_prop", type_prop_tr'), |
836 [("_type_prop", type_prop_tr'), |
837 ("\\<^const>TYPE", type_tr'), |
837 ("\\<^const>Pure.type", type_tr'), |
838 ("_type_constraint_", type_constraint_tr')]); |
838 ("_type_constraint_", type_constraint_tr')]); |
839 |
839 |
840 |
840 |
841 |
841 |
842 (** check/uncheck **) |
842 (** check/uncheck **) |