491 |> Proof_Context.add_assms_i Assumption.assume_export asms'; |
491 |> Proof_Context.add_assms_i Assumption.assume_export asms'; |
492 in ctxt' end) |
492 in ctxt' end) |
493 | init (Defines defs) = Context.map_proof (fn ctxt => |
493 | init (Defines defs) = Context.map_proof (fn ctxt => |
494 let |
494 let |
495 val defs' = Attrib.map_specs (map (Attrib.attribute ctxt)) defs; |
495 val defs' = Attrib.map_specs (map (Attrib.attribute ctxt)) defs; |
496 val asms = defs' |> map (fn ((name, atts), (t, ps)) => |
496 val asms = defs' |> map (fn (b, (t, ps)) => |
497 let val ((c, _), t') = Local_Defs.cert_def ctxt t (* FIXME adapt ps? *) |
497 let val (_, t') = Local_Defs.cert_def ctxt t (* FIXME adapt ps? *) |
498 in (t', ((Thm.def_binding_optional (Binding.name c) name, atts), [(t', ps)])) end); |
498 in (t', (b, [(t', ps)])) end); |
499 val (_, ctxt') = ctxt |
499 val (_, ctxt') = ctxt |
500 |> fold Variable.auto_fixes (map #1 asms) |
500 |> fold Variable.auto_fixes (map #1 asms) |
501 |> Proof_Context.add_assms_i Local_Defs.def_export (map #2 asms); |
501 |> Proof_Context.add_assms_i Local_Defs.def_export (map #2 asms); |
502 in ctxt' end) |
502 in ctxt' end) |
503 | init (Notes (kind, facts)) = Attrib.generic_notes kind facts #> #2; |
503 | init (Notes (kind, facts)) = Attrib.generic_notes kind facts #> #2; |
505 |
505 |
506 (* activate *) |
506 (* activate *) |
507 |
507 |
508 fun activate_i elem ctxt = |
508 fun activate_i elem ctxt = |
509 let |
509 let |
510 val elem' = map_ctxt_attrib Args.assignable elem; |
510 val elem' = |
|
511 (case map_ctxt_attrib Args.assignable elem of |
|
512 Defines defs => |
|
513 Defines (defs |> map (fn ((a, atts), (t, ps)) => |
|
514 ((Thm.def_binding_optional (Binding.name (#1 (#1 (Local_Defs.cert_def ctxt t)))) a, atts), |
|
515 (t, ps)))) |
|
516 | e => e); |
511 val ctxt' = Context.proof_map (init elem') ctxt; |
517 val ctxt' = Context.proof_map (init elem') ctxt; |
512 in (map_ctxt_attrib Args.closure elem', ctxt') end; |
518 in (map_ctxt_attrib Args.closure elem', ctxt') end; |
513 |
519 |
514 fun activate raw_elem ctxt = |
520 fun activate raw_elem ctxt = |
515 let val elem = raw_elem |> map_ctxt |
521 let val elem = raw_elem |> map_ctxt |