1165 fun update_case _ _ ("", _) res = res |
1165 fun update_case _ _ ("", _) res = res |
1166 | update_case _ _ (name, NONE) (cases, index) = |
1166 | update_case _ _ (name, NONE) (cases, index) = |
1167 (Name_Space.del_table name cases, index) |
1167 (Name_Space.del_table name cases, index) |
1168 | update_case context is_proper (name, SOME c) (cases, index) = |
1168 | update_case context is_proper (name, SOME c) (cases, index) = |
1169 let |
1169 let |
1170 val (_, cases') = cases |> Name_Space.define context false |
1170 val binding = |
1171 (Binding.make (name, Position.none), ((c, is_proper), index)); |
1171 Binding.make (name, Position.none) |
|
1172 |> not is_proper ? Binding.conceal; |
|
1173 val (_, cases') = cases |
|
1174 |> Name_Space.define context false (binding, ((c, is_proper), index)); |
1172 val index' = index + 1; |
1175 val index' = index + 1; |
1173 in (cases', index') end; |
1176 in (cases', index') end; |
1174 |
1177 |
1175 fun fix (b, T) ctxt = |
1178 fun fix (b, T) ctxt = |
1176 let val ([x], ctxt') = add_fixes [(b, SOME T, NoSyn)] ctxt |
1179 let val ([x], ctxt') = add_fixes [(b, SOME T, NoSyn)] ctxt |