diff -r a44b0fdaa6c2 -r b2c6033fc7e4 src/Pure/axclass.ML
--- a/src/Pure/axclass.ML	Mon Apr 18 13:52:23 2011 +0200
+++ b/src/Pure/axclass.ML	Mon Apr 18 14:05:39 2011 +0200
@@ -59,15 +59,12 @@
 
 type param = string * class;
 
-fun add_param pp ((x, c): param) params =
+fun add_param ctxt ((x, c): param) params =
   (case AList.lookup (op =) params x of
     NONE => (x, c) :: params
   | SOME c' =>
-      let val ctxt = Syntax.init_pretty pp in
-        error ("Duplicate class parameter " ^ quote x ^
-          " for " ^ Syntax.string_of_sort ctxt [c] ^
-          (if c = c' then "" else " and " ^ Syntax.string_of_sort ctxt [c']))
-      end);
+      error ("Duplicate class parameter " ^ quote x ^ " for " ^ Syntax.string_of_sort ctxt [c] ^
+        (if c = c' then "" else " and " ^ Syntax.string_of_sort ctxt [c'])));
 
 
 (* setup data *)
@@ -107,10 +104,14 @@
         proven_arities = proven_arities2, inst_params = inst_params2,
         diff_classrels = diff_classrels2}) =
     let
+      val ctxt = Syntax.init_pretty pp;
+
       val axclasses' = Symtab.merge (K true) (axclasses1, axclasses2);
       val params' =
         if null params1 then params2
-        else fold_rev (fn p => if member (op =) params1 p then I else add_param pp p) params2 params1;
+        else
+          fold_rev (fn p => if member (op =) params1 p then I else add_param ctxt p)
+            params2 params1;
 
       (*transitive closure of classrels and arity completion is done in Theory.at_begin hook*)
       val proven_classrels' = Symreltab.join (K #1) (proven_classrels1, proven_classrels2);
@@ -593,7 +594,7 @@
       |> #2
       |> Sign.restore_naming facts_thy
       |> map_axclasses (Symtab.update (class, axclass))
-      |> map_params (fold (fn (x, _) => add_param (Context.pretty ctxt) (x, class)) params);
+      |> map_params (fold (fn (x, _) => add_param ctxt (x, class)) params);
 
   in (class, result_thy) end;