equal
deleted
inserted
replaced
484 (** activate in context, return elements and facts **) |
484 (** activate in context, return elements and facts **) |
485 |
485 |
486 local |
486 local |
487 |
487 |
488 fun activate_elem (Fixes fixes) ctxt = |
488 fun activate_elem (Fixes fixes) ctxt = |
489 ctxt |> ProofContext.add_fixes_i fixes |> snd |
489 ctxt |> ProofContext.add_fixes fixes |> snd |
490 | activate_elem (Constrains _) ctxt = |
490 | activate_elem (Constrains _) ctxt = |
491 ctxt |
491 ctxt |
492 | activate_elem (Assumes asms) ctxt = |
492 | activate_elem (Assumes asms) ctxt = |
493 let |
493 let |
494 val asms' = Attrib.map_specs (Attrib.attribute_i (ProofContext.theory_of ctxt)) asms; |
494 val asms' = Attrib.map_specs (Attrib.attribute_i (ProofContext.theory_of ctxt)) asms; |