# HG changeset patch
# User wenzelm
# Date 1538256223 -7200
# Node ID 6f8ae6ddc26b01e147c57567f068e137b07a2e58
# Parent  0405d06f08f31237865a72cc4b168746e491bfd5
more direct locale goal: avoid renaming of type_parameters;

diff -r 0405d06f08f3 -r 6f8ae6ddc26b src/Pure/Thy/export_theory.ML
--- a/src/Pure/Thy/export_theory.ML	Sat Sep 29 21:05:32 2018 +0200
+++ b/src/Pure/Thy/export_theory.ML	Sat Sep 29 23:23:43 2018 +0200
@@ -105,23 +105,23 @@
 
 fun locale_content thy loc =
   let
-    val loc_ctxt = Locale.init loc thy;
-    val args = Locale.params_of thy loc
-      |> map (fn ((x, T), _) => ((x, T), get_syntax_param loc_ctxt loc x));
+    val ctxt = Locale.init loc thy;
+    val args =
+      Locale.params_of thy loc
+      |> map (fn ((x, T), _) => ((x, T), get_syntax_param ctxt loc x));
     val axioms =
       let
+        val (asm, defs) = Locale.specification_of thy loc;
+        val cprops = map (Thm.cterm_of ctxt) (the_list asm @ defs);
         val (intro1, intro2) = Locale.intros_of thy loc;
-        fun intros_tac ctxt = Method.try_intros_tac ctxt (the_list intro1 @ the_list intro2);
-        val inst = Expression.Named (args |> map (fn ((x, T), _) => (x, Free (x, T))));
+        val intros_tac = Method.try_intros_tac ctxt (the_list intro1 @ the_list intro2) [];
         val res =
-          Proof_Context.init_global thy
-          |> Interpretation.interpretation ([(loc, (("", false), (inst, [])))], [])
-          |> Proof.refine (Method.Basic (METHOD o intros_tac))
-          |> Seq.filter_results
+          Goal.init (Conjunction.mk_conjunction_balanced cprops)
+          |> (ALLGOALS Goal.conjunction_tac THEN intros_tac)
           |> try Seq.hd;
       in
         (case res of
-          SOME st => Thm.prems_of (#goal (Proof.goal st))
+          SOME goal => Thm.prems_of goal
         | NONE => raise Fail ("Cannot unfold locale " ^ quote loc))
       end;
     val typargs = rev (fold Term.add_tfrees (map (Free o #1) args @ axioms) []);