src/Pure/Isar/interpretation.ML
changeset 61772 2f33f6cc964d
parent 61771 acc532690ee1
child 61773 2256ef8224f6
equal deleted inserted replaced
61771:acc532690ee1 61772:2f33f6cc964d
    86       prep_mixins prep_term prep_prop expr_ctxt
    86       prep_mixins prep_term prep_prop expr_ctxt
    87         (fold Locale.activate_declarations deps expr_ctxt) raw_defs raw_eqns;
    87         (fold Locale.activate_declarations deps expr_ctxt) raw_defs raw_eqns;
    88     val (def_eqns, def_ctxt) = define_mixins pre_defs expr_ctxt;
    88     val (def_eqns, def_ctxt) = define_mixins pre_defs expr_ctxt;
    89     val attrss = map (apsnd (map (prep_attr def_ctxt)) o fst) raw_eqns;
    89     val attrss = map (apsnd (map (prep_attr def_ctxt)) o fst) raw_eqns;
    90     val goal_ctxt = fold Variable.auto_fixes eqns def_ctxt;
    90     val goal_ctxt = fold Variable.auto_fixes eqns def_ctxt;
    91     val export' = Variable.export_morphism goal_ctxt def_ctxt;
    91     val export' = Variable.export_morphism goal_ctxt expr_ctxt;
    92   in (((propss, deps, export, export'), (def_eqns, eqns, attrss)), goal_ctxt) end;
    92   in (((propss, deps, export, export'), (def_eqns, eqns, attrss)), goal_ctxt) end;
    93 
    93 
    94 in
    94 in
    95 
    95 
    96 fun cert_interpretation expression =
    96 fun cert_interpretation expression =