equal
deleted
inserted
replaced
75 Element.Notes (maps (Element.facts_of thy) elems') |
75 Element.Notes (maps (Element.facts_of thy) elems') |
76 |> Element.satisfy_ctxt prems'' |
76 |> Element.satisfy_ctxt prems'' |
77 |> Element.map_ctxt_values I I (ProofContext.export ctxt'' ctxt); |
77 |> Element.map_ctxt_values I I (ProofContext.export ctxt'' ctxt); |
78 (* FIXME export typs/terms *) |
78 (* FIXME export typs/terms *) |
79 |
79 |
80 val _ = PolyML.print notes; |
80 val _ = print notes; |
81 |
81 |
82 val notes' = notes |
82 val notes' = notes |
83 |> Attrib.map_facts (Attrib.attribute_i thy) |
83 |> Attrib.map_facts (Attrib.attribute_i thy) |
84 |> map (fn ((a, atts), facts) => ((a, atts @ more_atts), facts)); |
84 |> map (fn ((a, atts), facts) => ((a, atts @ more_atts), facts)); |
85 |
85 |