src/Pure/Thy/export_theory.ML
changeset 69086 2859dcdbc849
parent 69083 6f8ae6ddc26b
child 69087 06017b2c4552
     1.1 --- a/src/Pure/Thy/export_theory.ML	Sun Sep 30 09:00:11 2018 +0200
     1.2 +++ b/src/Pure/Thy/export_theory.ML	Sun Sep 30 11:58:59 2018 +0200
     1.3 @@ -130,7 +130,6 @@
     1.4  fun locale_dependency_subst thy (dep: Locale.locale_dependency) =
     1.5    let
     1.6      val (type_params, params) = Locale.parameters_of thy (#source dep);
     1.7 -    (* FIXME proper type_params wrt. locale_content (!?!) *)
     1.8      val typargs = fold (Term.add_tfreesT o #2 o #1) params type_params;
     1.9      val substT =
    1.10        typargs |> map_filter (fn v =>