src/Pure/Thy/export_theory.ML

   (fold_types o fold_atyps) (fn TFree (a, S) => is_free used a ? insert (op =) (a, S) | _ => I);
 
 
 (* locale content *)
 
-fun locale_content ctxt loc =
+fun locale_content thy loc =
   let
-    val thy = Proof_Context.theory_of ctxt;
-
     val args = map #1 (Locale.params_of thy loc);
     val axioms =
       let
         val (intro1, intro2) = Locale.intros_of thy loc;
         fun intros_tac ctxt = Method.try_intros_tac ctxt (the_list intro1 @ the_list intro2);

       in
         (case res of
           SOME st => Thm.prems_of (#goal (Proof.goal st))
         | NONE => raise Fail ("Cannot unfold locale " ^ quote loc))
       end;
-
     val typargs = rev (fold Term.add_tfrees (map Free args @ axioms) []);
-    val typargs_dups =
-      AList.group (op =) typargs |> filter (fn (_, [_]) => false | _ => true)
-        |> maps (fn (x, ys) => map (pair x) ys);
-    val typargs_print = Syntax.string_of_typ (Config.put show_sorts true ctxt) o TFree;
-    val _ =
-      if null typargs_dups then ()
-      else error ("Duplicate type parameters " ^ commas (map typargs_print typargs_dups));
   in {typargs = typargs, args = args, axioms = axioms} end;
 
 
 (* general setup *)
 

       let open XML.Encode Term_XML.Encode
       in triple (list (pair string sort)) (list (pair string typ)) (list (encode_axiom used)) end;
 
     fun export_locale loc =
       let
-        val {typargs, args, axioms} = locale_content thy_ctxt loc;
+        val {typargs, args, axioms} = locale_content thy loc;
         val used = fold Name.declare (map #1 typargs @ map #1 args) Name.context;
       in encode_locale used (typargs, args, axioms) end
       handle ERROR msg =>
         cat_error msg ("The error(s) above occurred in locale " ^
           quote (Locale.markup_name thy_ctxt loc));