src/Pure/Thy/export_theory.ML
changeset 69083 6f8ae6ddc26b
parent 69077 11529ae45786
child 69086 2859dcdbc849
     1.1 --- a/src/Pure/Thy/export_theory.ML	Sat Sep 29 21:05:32 2018 +0200
     1.2 +++ b/src/Pure/Thy/export_theory.ML	Sat Sep 29 23:23:43 2018 +0200
     1.3 @@ -105,23 +105,23 @@
     1.4  
     1.5  fun locale_content thy loc =
     1.6    let
     1.7 -    val loc_ctxt = Locale.init loc thy;
     1.8 -    val args = Locale.params_of thy loc
     1.9 -      |> map (fn ((x, T), _) => ((x, T), get_syntax_param loc_ctxt loc x));
    1.10 +    val ctxt = Locale.init loc thy;
    1.11 +    val args =
    1.12 +      Locale.params_of thy loc
    1.13 +      |> map (fn ((x, T), _) => ((x, T), get_syntax_param ctxt loc x));
    1.14      val axioms =
    1.15        let
    1.16 +        val (asm, defs) = Locale.specification_of thy loc;
    1.17 +        val cprops = map (Thm.cterm_of ctxt) (the_list asm @ defs);
    1.18          val (intro1, intro2) = Locale.intros_of thy loc;
    1.19 -        fun intros_tac ctxt = Method.try_intros_tac ctxt (the_list intro1 @ the_list intro2);
    1.20 -        val inst = Expression.Named (args |> map (fn ((x, T), _) => (x, Free (x, T))));
    1.21 +        val intros_tac = Method.try_intros_tac ctxt (the_list intro1 @ the_list intro2) [];
    1.22          val res =
    1.23 -          Proof_Context.init_global thy
    1.24 -          |> Interpretation.interpretation ([(loc, (("", false), (inst, [])))], [])
    1.25 -          |> Proof.refine (Method.Basic (METHOD o intros_tac))
    1.26 -          |> Seq.filter_results
    1.27 +          Goal.init (Conjunction.mk_conjunction_balanced cprops)
    1.28 +          |> (ALLGOALS Goal.conjunction_tac THEN intros_tac)
    1.29            |> try Seq.hd;
    1.30        in
    1.31          (case res of
    1.32 -          SOME st => Thm.prems_of (#goal (Proof.goal st))
    1.33 +          SOME goal => Thm.prems_of goal
    1.34          | NONE => raise Fail ("Cannot unfold locale " ^ quote loc))
    1.35        end;
    1.36      val typargs = rev (fold Term.add_tfrees (map (Free o #1) args @ axioms) []);