equal
deleted
inserted
replaced
93 fun annbexp_tr' name (r :: (Const ("Collect", _) $ t) :: ts) = |
93 fun annbexp_tr' name (r :: (Const ("Collect", _) $ t) :: ts) = |
94 annquote_tr' (Syntax.const name) (r :: t :: ts) |
94 annquote_tr' (Syntax.const name) (r :: t :: ts) |
95 | annbexp_tr' _ _ = raise Match; |
95 | annbexp_tr' _ _ = raise Match; |
96 |
96 |
97 fun upd_tr' (x_upd, T) = |
97 fun upd_tr' (x_upd, T) = |
98 (case try (unsuffix RecordPackage.updateN) x_upd of |
98 (case try (unsuffix Record.updateN) x_upd of |
99 SOME x => (x, if T = dummyT then T else Term.domain_type T) |
99 SOME x => (x, if T = dummyT then T else Term.domain_type T) |
100 | NONE => raise Match); |
100 | NONE => raise Match); |
101 |
101 |
102 fun update_name_tr' (Free x) = Free (upd_tr' x) |
102 fun update_name_tr' (Free x) = Free (upd_tr' x) |
103 | update_name_tr' ((c as Const ("_free", _)) $ Free x) = |
103 | update_name_tr' ((c as Const ("_free", _)) $ Free x) = |