equal
deleted
inserted
replaced
55 fun prep_interpretation prep_expr prep_term prep_prop prep_attr expression raw_defs raw_eqns initial_ctxt = |
55 fun prep_interpretation prep_expr prep_term prep_prop prep_attr expression raw_defs raw_eqns initial_ctxt = |
56 let |
56 let |
57 (*reading*) |
57 (*reading*) |
58 val ((propss, deps, export), expr_ctxt) = prep_expr expression initial_ctxt; |
58 val ((propss, deps, export), expr_ctxt) = prep_expr expression initial_ctxt; |
59 val deps_ctxt = fold Locale.activate_declarations deps expr_ctxt; |
59 val deps_ctxt = fold Locale.activate_declarations deps expr_ctxt; |
60 val prep = Syntax.check_terms deps_ctxt #> Variable.export_terms deps_ctxt deps_ctxt; |
60 val prep = Syntax.check_terms deps_ctxt #> Variable.export_terms deps_ctxt expr_ctxt; |
61 val rhss = (prep o map (prep_term deps_ctxt o snd o snd)) raw_defs; |
61 val rhss = (prep o map (prep_term deps_ctxt o snd o snd)) raw_defs; |
62 val eqns = (prep o map (prep_prop deps_ctxt o snd)) raw_eqns; |
62 val eqns = (prep o map (prep_prop deps_ctxt o snd)) raw_eqns; |
63 |
63 |
64 (*defining*) |
64 (*defining*) |
65 val pre_defs = map2 (fn ((name, atts), ((b, mx), _)) => fn rhs => |
65 val pre_defs = map2 (fn ((name, atts), ((b, mx), _)) => fn rhs => |