22 | change_arrow _ T = raise TYPE ("cont_consts: change_arrow", [T], []) |
22 | change_arrow _ T = raise TYPE ("cont_consts: change_arrow", [T], []) |
23 |
23 |
24 fun trans_rules name2 name1 n mx = |
24 fun trans_rules name2 name1 n mx = |
25 let |
25 let |
26 val vnames = Name.invents Name.context "a" n |
26 val vnames = Name.invents Name.context "a" n |
27 val extra_parse_rule = Syntax.Parse_Rule (Constant name2, Constant name1) |
27 val extra_parse_rule = Syntax.Parse_Rule (Ast.Constant name2, Ast.Constant name1) |
28 in |
28 in |
29 [Syntax.Parse_Print_Rule |
29 [Syntax.Parse_Print_Rule |
30 (Syntax.mk_appl (Constant name2) (map Variable vnames), |
30 (Ast.mk_appl (Ast.Constant name2) (map Ast.Variable vnames), |
31 fold (fn a => fn t => Syntax.mk_appl (Constant @{const_syntax Rep_cfun}) [t, Variable a]) |
31 fold (fn a => fn t => |
32 vnames (Constant name1))] @ |
32 Ast.mk_appl (Ast.Constant @{const_syntax Rep_cfun}) [t, Ast.Variable a]) |
|
33 vnames (Ast.Constant name1))] @ |
33 (case mx of |
34 (case mx of |
34 Infix _ => [extra_parse_rule] |
35 Infix _ => [extra_parse_rule] |
35 | Infixl _ => [extra_parse_rule] |
36 | Infixl _ => [extra_parse_rule] |
36 | Infixr _ => [extra_parse_rule] |
37 | Infixr _ => [extra_parse_rule] |
37 | _ => []) |
38 | _ => []) |