obsolete (see aec64b88e708);
authorwenzelm
Sat Sep 22 15:22:29 2018 +0200 (13 months ago)
changeset 69034855c3c501b09
parent 69033 c5db368833b1
child 69035 d75cd481f8d9
obsolete (see aec64b88e708);
src/Pure/Thy/export_theory.ML
     1.1 --- a/src/Pure/Thy/export_theory.ML	Sat Sep 22 14:24:53 2018 +0200
     1.2 +++ b/src/Pure/Thy/export_theory.ML	Sat Sep 22 15:22:29 2018 +0200
     1.3 @@ -72,10 +72,8 @@
     1.4  
     1.5  (* locale content *)
     1.6  
     1.7 -fun locale_content ctxt loc =
     1.8 +fun locale_content thy loc =
     1.9    let
    1.10 -    val thy = Proof_Context.theory_of ctxt;
    1.11 -
    1.12      val args = map #1 (Locale.params_of thy loc);
    1.13      val axioms =
    1.14        let
    1.15 @@ -93,15 +91,7 @@
    1.16            SOME st => Thm.prems_of (#goal (Proof.goal st))
    1.17          | NONE => raise Fail ("Cannot unfold locale " ^ quote loc))
    1.18        end;
    1.19 -
    1.20      val typargs = rev (fold Term.add_tfrees (map Free args @ axioms) []);
    1.21 -    val typargs_dups =
    1.22 -      AList.group (op =) typargs |> filter (fn (_, [_]) => false | _ => true)
    1.23 -        |> maps (fn (x, ys) => map (pair x) ys);
    1.24 -    val typargs_print = Syntax.string_of_typ (Config.put show_sorts true ctxt) o TFree;
    1.25 -    val _ =
    1.26 -      if null typargs_dups then ()
    1.27 -      else error ("Duplicate type parameters " ^ commas (map typargs_print typargs_dups));
    1.28    in {typargs = typargs, args = args, axioms = axioms} end;
    1.29  
    1.30  
    1.31 @@ -290,7 +280,7 @@
    1.32  
    1.33      fun export_locale loc =
    1.34        let
    1.35 -        val {typargs, args, axioms} = locale_content thy_ctxt loc;
    1.36 +        val {typargs, args, axioms} = locale_content thy loc;
    1.37          val used = fold Name.declare (map #1 typargs @ map #1 args) Name.context;
    1.38        in encode_locale used (typargs, args, axioms) end
    1.39        handle ERROR msg =>