equal
deleted
inserted
replaced
86 val export' = Variable.export_morphism goal_ctxt def_ctxt; |
86 val export' = Variable.export_morphism goal_ctxt def_ctxt; |
87 in (((propss, deps, export, export'), (def_eqns, eqns, attrss)), goal_ctxt) end; |
87 in (((propss, deps, export, export'), (def_eqns, eqns, attrss)), goal_ctxt) end; |
88 |
88 |
89 in |
89 in |
90 |
90 |
91 val cert_interpretation = |
91 fun cert_interpretation expression = |
92 prep_interpretation Expression.cert_goal_expression (K I) (K I) (K I); |
92 prep_interpretation Expression.cert_goal_expression (K I) (K I) (K I) expression; |
93 |
93 |
94 val read_interpretation = |
94 fun read_interpretation expression = |
95 prep_interpretation Expression.read_goal_expression Syntax.parse_term Syntax.parse_prop Attrib.check_src; |
95 prep_interpretation Expression.read_goal_expression Syntax.parse_term |
|
96 Syntax.parse_prop Attrib.check_src expression; |
96 |
97 |
97 end; |
98 end; |
98 |
99 |
99 |
100 |
100 (* interpretation machinery *) |
101 (* interpretation machinery *) |