65 |
65 |
66 fun bexp_tr' name ((Const (@{const_syntax Collect}, _) $ t) :: ts) = |
66 fun bexp_tr' name ((Const (@{const_syntax Collect}, _) $ t) :: ts) = |
67 quote_tr' (Syntax.const name) (t :: ts) |
67 quote_tr' (Syntax.const name) (t :: ts) |
68 | bexp_tr' _ _ = raise Match; |
68 | bexp_tr' _ _ = raise Match; |
69 |
69 |
70 fun K_tr' (Abs (_, _, t)) = |
|
71 if null (loose_bnos t) then t else raise Match |
|
72 | K_tr' (Abs (_, _, Abs (_, _, t) $ Bound 0)) = |
|
73 if null (loose_bnos t) then t else raise Match |
|
74 | K_tr' _ = raise Match; |
|
75 |
|
76 fun assign_tr' (Abs (x, _, f $ k $ Bound 0) :: ts) = |
70 fun assign_tr' (Abs (x, _, f $ k $ Bound 0) :: ts) = |
77 quote_tr' (Syntax.const @{syntax_const "_Assign"} $ Syntax.update_name_tr' f) |
71 quote_tr' (Syntax.const @{syntax_const "_Assign"} $ Syntax.update_name_tr' f) |
78 (Abs (x, dummyT, K_tr' k) :: ts) |
72 (Abs (x, dummyT, Syntax.const_abs_tr' k) :: ts) |
79 | assign_tr' _ = raise Match; |
73 | assign_tr' _ = raise Match; |
80 in |
74 in |
81 [(@{const_syntax Collect}, assert_tr'), |
75 [(@{const_syntax Collect}, assert_tr'), |
82 (@{const_syntax Basic}, assign_tr'), |
76 (@{const_syntax Basic}, assign_tr'), |
83 (@{const_syntax Cond}, bexp_tr' @{syntax_const "_Cond"}), |
77 (@{const_syntax Cond}, bexp_tr' @{syntax_const "_Cond"}), |