--- a/src/Pure/type.ML Mon Apr 18 12:11:58 2011 +0200
+++ b/src/Pure/type.ML Mon Apr 18 13:26:39 2011 +0200
@@ -86,17 +86,16 @@
val eq_type: tyenv -> typ * typ -> bool
(*extend and merge type signatures*)
- val add_class: Proof.context -> Context.pretty -> Name_Space.naming ->
- binding * class list -> tsig -> tsig
+ val add_class: Proof.context -> Name_Space.naming -> binding * class list -> tsig -> tsig
val hide_class: bool -> string -> tsig -> tsig
val set_defsort: sort -> tsig -> tsig
val add_type: Proof.context -> Name_Space.naming -> binding * int -> tsig -> tsig
val add_abbrev: Proof.context -> Name_Space.naming -> binding * string list * typ -> tsig -> tsig
val add_nonterminal: Proof.context -> Name_Space.naming -> binding -> tsig -> tsig
val hide_type: bool -> string -> tsig -> tsig
- val add_arity: Context.pretty -> arity -> tsig -> tsig
- val add_classrel: Context.pretty -> class * class -> tsig -> tsig
- val merge_tsig: Context.pretty -> tsig * tsig -> tsig
+ val add_arity: Proof.context -> arity -> tsig -> tsig
+ val add_classrel: Proof.context -> class * class -> tsig -> tsig
+ val merge_tsig: Proof.context -> tsig * tsig -> tsig
end;
structure Type: TYPE =
@@ -577,14 +576,14 @@
(* classes *)
-fun add_class ctxt pp naming (c, cs) tsig =
+fun add_class ctxt naming (c, cs) tsig =
tsig |> map_tsig (fn ((space, classes), default, types) =>
let
val cs' = map (cert_class tsig) cs
handle TYPE (msg, _, _) => error msg;
val _ = Binding.check c;
val (c', space') = space |> Name_Space.declare ctxt true naming c;
- val classes' = classes |> Sorts.add_class pp (c', cs');
+ val classes' = classes |> Sorts.add_class ctxt (c', cs');
in ((space', classes'), default, types) end);
fun hide_class fully c = map_tsig (fn ((space, classes), default, types) =>
@@ -593,7 +592,7 @@
(* arities *)
-fun add_arity pp (t, Ss, S) tsig = tsig |> map_tsig (fn ((space, classes), default, types) =>
+fun add_arity ctxt (t, Ss, S) tsig = tsig |> map_tsig (fn ((space, classes), default, types) =>
let
val _ =
(case lookup_type tsig t of
@@ -602,18 +601,18 @@
| NONE => error (undecl_type t));
val (Ss', S') = (map (cert_sort tsig) Ss, cert_sort tsig S)
handle TYPE (msg, _, _) => error msg;
- val classes' = classes |> Sorts.add_arities pp ((t, map (fn c' => (c', Ss')) S'));
+ val classes' = classes |> Sorts.add_arities ctxt ((t, map (fn c' => (c', Ss')) S'));
in ((space, classes'), default, types) end);
(* classrel *)
-fun add_classrel pp rel tsig =
+fun add_classrel ctxt rel tsig =
tsig |> map_tsig (fn ((space, classes), default, types) =>
let
val rel' = pairself (cert_class tsig) rel
handle TYPE (msg, _, _) => error msg;
- val classes' = classes |> Sorts.add_classrel pp rel';
+ val classes' = classes |> Sorts.add_classrel ctxt rel';
in ((space, classes'), default, types) end);
@@ -674,7 +673,7 @@
(* merge type signatures *)
-fun merge_tsig pp (tsig1, tsig2) =
+fun merge_tsig ctxt (tsig1, tsig2) =
let
val (TSig {classes = (space1, classes1), default = default1, types = types1,
log_types = _}) = tsig1;
@@ -682,7 +681,7 @@
log_types = _}) = tsig2;
val space' = Name_Space.merge (space1, space2);
- val classes' = Sorts.merge_algebra pp (classes1, classes2);
+ val classes' = Sorts.merge_algebra ctxt (classes1, classes2);
val default' = Sorts.inter_sort classes' (default1, default2);
val types' = Name_Space.merge_tables (types1, types2);
in build_tsig ((space', classes'), default', types') end;