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