pass plain Proof.context for pretty printing;

--- 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;
 

--- a/src/Pure/defs.ML	Mon Apr 18 13:52:23 2011 +0200
+++ b/src/Pure/defs.ML	Mon Apr 18 14:05:39 2011 +0200
@@ -18,7 +18,7 @@
    {restricts: ((string * typ list) * string) list,
     reducts: ((string * typ list) * (string * typ list) list) list}
   val empty: T
-  val merge: Context.pretty -> T * T -> T
+  val merge: Proof.context -> T * T -> T
   val define: Proof.context -> bool -> string option -> string ->
     string * typ list -> (string * typ list) list -> T -> T
 end
@@ -187,9 +187,8 @@
 
 (* merge *)
 
-fun merge pp (Defs defs1, Defs defs2) =
+fun merge ctxt (Defs defs1, Defs defs2) =
   let
-    val ctxt = Syntax.init_pretty pp;
     fun add_deps (c, args) restr deps defs =
       if AList.defined (op =) (reducts_of defs c) args then defs
       else dependencies ctxt (c, args) restr deps defs;

--- a/src/Pure/theory.ML	Mon Apr 18 13:52:23 2011 +0200
+++ b/src/Pure/theory.ML	Mon Apr 18 14:05:39 2011 +0200
@@ -95,11 +95,12 @@
 
   fun merge pp (thy1, thy2) =
     let
+      val ctxt = Syntax.init_pretty pp;
       val Thy {axioms = _, defs = defs1, wrappers = (bgs1, ens1)} = thy1;
       val Thy {axioms = _, defs = defs2, wrappers = (bgs2, ens2)} = thy2;
 
       val axioms' = empty_axioms;
-      val defs' = Defs.merge pp (defs1, defs2);
+      val defs' = Defs.merge ctxt (defs1, defs2);
       val bgs' = Library.merge (eq_snd op =) (bgs1, bgs2);
       val ens' = Library.merge (eq_snd op =) (ens1, ens2);
     in make_thy (axioms', defs', (bgs', ens')) end;