equal
deleted
inserted
replaced
118 (* translation rules *) |
118 (* translation rules *) |
119 |
119 |
120 fun read_trrules thy raw_rules = |
120 fun read_trrules thy raw_rules = |
121 let |
121 let |
122 val ctxt = Proof_Context.init_global thy; |
122 val ctxt = Proof_Context.init_global thy; |
|
123 val read_root = |
|
124 #1 o dest_Type o Proof_Context.read_type_name {proper = true, strict = false} ctxt; |
123 in |
125 in |
124 raw_rules |> map (Syntax.map_trrule (fn (r, s) => |
126 raw_rules |
125 Syntax_Phases.parse_ast_pattern ctxt (Proof_Context.intern_type ctxt r, s))) |
127 |> map (Syntax.map_trrule (fn (r, s) => Syntax_Phases.parse_ast_pattern ctxt (read_root r, s))) |
126 end; |
128 end; |
127 |
129 |
128 fun translations args thy = Sign.add_trrules (read_trrules thy args) thy; |
130 fun translations args thy = Sign.add_trrules (read_trrules thy args) thy; |
129 fun no_translations args thy = Sign.del_trrules (read_trrules thy args) thy; |
131 fun no_translations args thy = Sign.del_trrules (read_trrules thy args) thy; |
130 |
132 |