src/Pure/Tools/class_package.ML

     fun interpret name_locale cs ax_axioms thy =
       thy
       |> Locale.interpretation (NameSpace.base name_locale, [])
            (Locale.Locale name_locale)
              (map (fn ((c, _), _) => SOME (Sign.intern_const thy c)) cs)
-      |> Proof.global_terminal_proof (Method.Basic (Method.fact ax_axioms), NONE)
-      |> swap;
+      |> Proof.global_terminal_proof (Method.Basic (Method.fact ax_axioms), NONE);
     fun print_ctxt ctxt elem = 
       map Pretty.writeln (Element.pretty_ctxt ctxt elem)
   in
     thy
     |> add_locale bname locexpr raw_body

   OuterSyntax.command classK "operational type classes" K.thy_decl
     (P.name --| P.$$$ "="
      -- Scan.optional (Scan.repeat1 (P.name --| P.$$$ "+")) []
      -- Scan.optional (P.!!! (Scan.repeat1 P.context_element)) []
       >> (Toplevel.theory_context
-          o (fn f => swap o f) o (fn ((bname, supclasses), elems) => add_class bname supclasses elems)));
+          o (fn ((bname, supclasses), elems) => add_class bname supclasses elems)));
 
 val instanceP =
   OuterSyntax.command instanceK "declare instance for operational type class" K.thy_goal
     (P.xname -- (P.$$$ "::" |-- P.!!! P.arity)
       -- Scan.repeat1 P.spec_name