724 (a, [([Assumption.assume (cterm_of thy def)], |
724 (a, [([Assumption.assume (cterm_of thy def)], |
725 [(Attrib.internal o K) Locale.witness_attrib])])) defs) |
725 [(Attrib.internal o K) Locale.witness_attrib])])) defs) |
726 | defines_to_notes _ e = e; |
726 | defines_to_notes _ e = e; |
727 |
727 |
728 fun gen_add_locale prep_decl |
728 fun gen_add_locale prep_decl |
729 bname raw_predicate_bname raw_imprt raw_body thy = |
729 bname raw_predicate_bname raw_import raw_body thy = |
730 let |
730 let |
731 val name = Sign.full_bname thy bname; |
731 val name = Sign.full_bname thy bname; |
732 val _ = Locale.defined thy name andalso |
732 val _ = Locale.defined thy name andalso |
733 error ("Duplicate definition of locale " ^ quote name); |
733 error ("Duplicate definition of locale " ^ quote name); |
734 |
734 |
735 val ((fixed, deps, body_elems), (parms, ctxt')) = |
735 val ((fixed, deps, body_elems), (parms, ctxt')) = |
736 prep_decl raw_imprt I raw_body (ProofContext.init thy); |
736 prep_decl raw_import I raw_body (ProofContext.init thy); |
737 val text as (((_, exts'), _), defs) = eval ctxt' deps body_elems; |
737 val text as (((_, exts'), _), defs) = eval ctxt' deps body_elems; |
738 |
738 |
739 val predicate_bname = if raw_predicate_bname = "" then bname |
739 val predicate_bname = if raw_predicate_bname = "" then bname |
740 else raw_predicate_bname; |
740 else raw_predicate_bname; |
741 val ((a_statement, a_intro, a_axioms), (b_statement, b_intro, b_axioms), thy') = |
741 val ((a_statement, a_intro, a_axioms), (b_statement, b_intro, b_axioms), thy') = |