equal
deleted
inserted
replaced
589 val asm' = Option.map (Morphism.term morph) asm; |
589 val asm' = Option.map (Morphism.term morph) asm; |
590 val defs' = map (Morphism.term morph) defs; |
590 val defs' = map (Morphism.term morph) defs; |
591 val text' = |
591 val text' = |
592 text |> |
592 text |> |
593 (if is_some asm then |
593 (if is_some asm then |
594 eval_text ctxt false (Assumes [(Attrib.empty_binding, [(the asm', [])])]) |
594 eval_text ctxt false (Assumes [(Binding.empty_atts, [(the asm', [])])]) |
595 else I) |> |
595 else I) |> |
596 (if not (null defs) then |
596 (if not (null defs) then |
597 eval_text ctxt false (Defines (map (fn def => (Attrib.empty_binding, (def, []))) defs')) |
597 eval_text ctxt false (Defines (map (fn def => (Binding.empty_atts, (def, []))) defs')) |
598 else I) |
598 else I) |
599 (* FIXME clone from locale.ML *) |
599 (* FIXME clone from locale.ML *) |
600 in text' end; |
600 in text' end; |
601 |
601 |
602 fun eval_elem ctxt elem text = |
602 fun eval_elem ctxt elem text = |