equal
deleted
inserted
replaced
45 declaration with the original name, type ...=>..., and the original mixfix |
45 declaration with the original name, type ...=>..., and the original mixfix |
46 is generated and connected to the other declaration via some translation. |
46 is generated and connected to the other declaration via some translation. |
47 *) |
47 *) |
48 fun transform thy (c, T, mx) = |
48 fun transform thy (c, T, mx) = |
49 let |
49 let |
50 fun syntax b = Syntax.mark_const (Sign.full_bname thy b) |
50 fun syntax b = Lexicon.mark_const (Sign.full_bname thy b) |
51 val c1 = Binding.name_of c |
51 val c1 = Binding.name_of c |
52 val c2 = c1 ^ "_cont_syntax" |
52 val c2 = c1 ^ "_cont_syntax" |
53 val n = Mixfix.mixfix_args mx |
53 val n = Mixfix.mixfix_args mx |
54 in |
54 in |
55 ((c, T, NoSyn), |
55 ((c, T, NoSyn), |