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