diff -r 93413dcee45b -r d42708f5c186 src/Pure/Tools/class_package.ML
--- a/src/Pure/Tools/class_package.ML	Fri Jan 27 19:03:09 2006 +0100
+++ b/src/Pure/Tools/class_package.ML	Fri Jan 27 19:03:10 2006 +0100
@@ -214,8 +214,7 @@
       |> 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
@@ -473,7 +472,7 @@
      -- 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