--- a/src/Pure/axclass.ML Sun Apr 17 23:47:05 2011 +0200
+++ b/src/Pure/axclass.ML Mon Apr 18 11:13:29 2011 +0200
@@ -62,9 +62,12 @@
fun add_param pp ((x, c): param) params =
(case AList.lookup (op =) params x of
NONE => (x, c) :: params
- | SOME c' => error ("Duplicate class parameter " ^ quote x ^
- " for " ^ Pretty.string_of_sort pp [c] ^
- (if c = c' then "" else " and " ^ Pretty.string_of_sort pp [c'])));
+ | 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);
(* setup data *)
@@ -590,7 +593,7 @@
|> #2
|> Sign.restore_naming facts_thy
|> map_axclasses (Symtab.update (class, axclass))
- |> map_params (fold (fn (x, _) => add_param (Syntax.pp ctxt) (x, class)) params);
+ |> map_params (fold (fn (x, _) => add_param (Context.pretty ctxt) (x, class)) params);
in (class, result_thy) end;