--- a/src/HOL/Nominal/nominal_datatype.ML Mon Apr 18 13:26:39 2011 +0200
+++ b/src/HOL/Nominal/nominal_datatype.ML Mon Apr 18 13:52:23 2011 +0200
@@ -211,7 +211,7 @@
val tyvars = map (map (fn s =>
(s, the (AList.lookup (op =) sorts s))) o #1) dts';
- fun inter_sort thy S S' = Type.inter_sort (Sign.tsig_of thy) (S, S');
+ fun inter_sort thy S S' = Sign.inter_sort thy (S, S');
fun augment_sort_typ thy S =
let val S = Sign.minimize_sort thy (Sign.certify_sort thy S)
in map_type_tfree (fn (s, S') => TFree (s,
--- a/src/HOL/Tools/Function/partial_function.ML Mon Apr 18 13:26:39 2011 +0200
+++ b/src/HOL/Tools/Function/partial_function.ML Mon Apr 18 13:52:23 2011 +0200
@@ -125,7 +125,7 @@
val thy = Proof_Context.theory_of ctxt;
val T = domain_type (fastype_of t);
val T' = fastype_of u;
- val subst = Type.typ_match (Sign.tsig_of thy) (T, T') Vartab.empty
+ val subst = Sign.typ_match thy (T, T') Vartab.empty
handle Type.TYPE_MATCH => raise TYPE ("apply_inst", [T, T'], [t, u])
in
map_types (Envir.norm_type subst) t $ u
--- a/src/HOL/Tools/enriched_type.ML Mon Apr 18 13:26:39 2011 +0200
+++ b/src/HOL/Tools/enriched_type.ML Mon Apr 18 13:52:23 2011 +0200
@@ -218,10 +218,11 @@
val qualify = Binding.qualify true prfx o Binding.name;
fun mapper_declaration comp_thm id_thm phi context =
let
- val typ_instance = Type.typ_instance (Proof_Context.tsig_of (Context.proof_of context));
+ val typ_instance = Sign.typ_instance (Context.theory_of context);
val mapper' = Morphism.term phi mapper;
val T_T' = pairself fastype_of (mapper, mapper');
- in if typ_instance T_T' andalso typ_instance (swap T_T')
+ in
+ if typ_instance T_T' andalso typ_instance (swap T_T')
then (Data.map o Symtab.cons_list) (tyco,
{ mapper = mapper', variances = variances,
comp = Morphism.thm phi comp_thm, id = Morphism.thm phi id_thm }) context
--- a/src/Pure/Isar/class.ML Mon Apr 18 13:26:39 2011 +0200
+++ b/src/Pure/Isar/class.ML Mon Apr 18 13:52:23 2011 +0200
@@ -540,10 +540,10 @@
NONE => NONE
| SOME ts' => SOME (ts', ctxt));
val lookup_inst_param = AxClass.lookup_inst_param consts params;
- val typ_instance = Type.typ_instance (Sign.tsig_of thy);
- fun improve (c, ty) = case lookup_inst_param (c, ty)
- of SOME (_, ty') => if typ_instance (ty', ty) then SOME (ty, ty') else NONE
- | NONE => NONE;
+ fun improve (c, ty) =
+ (case lookup_inst_param (c, ty) of
+ SOME (_, ty') => if Sign.typ_instance thy (ty', ty) then SOME (ty, ty') else NONE
+ | NONE => NONE);
in
thy
|> Theory.checkpoint
--- a/src/Pure/Isar/overloading.ML Mon Apr 18 13:26:39 2011 +0200
+++ b/src/Pure/Isar/overloading.ML Mon Apr 18 13:52:23 2011 +0200
@@ -63,20 +63,25 @@
fun improve_term_check ts ctxt =
let
+ val thy = Proof_Context.theory_of ctxt;
+
val { secondary_constraints, improve, subst, consider_abbrevs, passed, ... } =
ImprovableSyntax.get ctxt;
- val tsig = (Sign.tsig_of o Proof_Context.theory_of) ctxt;
val is_abbrev = consider_abbrevs andalso Proof_Context.abbrev_mode ctxt;
val passed_or_abbrev = passed orelse is_abbrev;
- fun accumulate_improvements (Const (c, ty)) = (case improve (c, ty)
- of SOME ty_ty' => Type.typ_match tsig ty_ty'
+ fun accumulate_improvements (Const (c, ty)) =
+ (case improve (c, ty) of
+ SOME ty_ty' => Sign.typ_match thy ty_ty'
| _ => I)
| accumulate_improvements _ = I;
val improvements = (fold o fold_aterms) accumulate_improvements ts Vartab.empty;
val ts' = (map o map_types) (Envir.subst_type improvements) ts;
- fun apply_subst t = Envir.expand_term (fn Const (c, ty) => (case subst (c, ty)
- of SOME (ty', t') =>
- if Type.typ_instance tsig (ty, ty')
+ fun apply_subst t =
+ Envir.expand_term
+ (fn Const (c, ty) =>
+ (case subst (c, ty) of
+ SOME (ty', t') =>
+ if Sign.typ_instance thy (ty, ty')
then SOME (ty', apply_subst t') else NONE
| NONE => NONE)
| _ => NONE) t;
--- a/src/Pure/sign.ML Mon Apr 18 13:26:39 2011 +0200
+++ b/src/Pure/sign.ML Mon Apr 18 13:52:23 2011 +0200
@@ -246,9 +246,9 @@
val arity_number = Type.arity_number o tsig_of;
fun arity_sorts thy = Type.arity_sorts (Context.pretty_global thy) (tsig_of thy);
-val certify_class = Type.cert_class o tsig_of;
-val certify_sort = Type.cert_sort o tsig_of;
-val certify_typ = Type.cert_typ o tsig_of;
+val certify_class = Type.cert_class o tsig_of;
+val certify_sort = Type.cert_sort o tsig_of;
+val certify_typ = Type.cert_typ o tsig_of;
fun certify_typ_mode mode = Type.cert_typ_mode mode o tsig_of;
--- a/src/Tools/subtyping.ML Mon Apr 18 13:26:39 2011 +0200
+++ b/src/Tools/subtyping.ML Mon Apr 18 13:52:23 2011 +0200
@@ -276,11 +276,11 @@
fun process_constraints ctxt err cs tye_idx =
let
+ val thy = Proof_Context.theory_of ctxt;
+
val coes_graph = coes_graph_of ctxt;
val tmaps = tmaps_of ctxt;
- val tsig = Sign.tsig_of (Proof_Context.theory_of ctxt);
- val arity_sorts = Type.arity_sorts (Context.pretty ctxt) tsig;
- val subsort = Type.subsort tsig;
+ val arity_sorts = Type.arity_sorts (Context.pretty ctxt) (Sign.tsig_of thy);
fun split_cs _ [] = ([], [])
| split_cs f (c :: cs) =
@@ -357,7 +357,7 @@
val (ch, done') = split_cs (test_update o Type_Infer.deref tye') done;
val todo' = ch @ todo;
in
- if subsort (S', S) (*TODO check this*)
+ if Sign.subsort thy (S', S) (*TODO check this*)
then simplify done' todo' (tye', idx)
else error (gen_msg err "sort mismatch")
end
@@ -429,7 +429,7 @@
fun adjust T U = if super then (T, U) else (U, T);
fun styp_test U Ts = forall
(fn T => T = U orelse Graph.is_edge coes_graph (adjust U T)) Ts;
- fun fitting Ts S U = Type.of_sort tsig (t_of U, S) andalso styp_test U Ts
+ fun fitting Ts S U = Sign.of_sort thy (t_of U, S) andalso styp_test U Ts
in
forall (fn (Ts, S) => exists (fitting Ts S) (T :: styps super T)) styps_and_sorts
end;
@@ -446,7 +446,7 @@
*)
fun tightest sup S styps_and_sorts (T :: Ts) =
let
- fun restriction T = Type.of_sort tsig (t_of T, S)
+ fun restriction T = Sign.of_sort thy (t_of T, S)
andalso ex_styp_of_sort (not sup) T styps_and_sorts;
fun candidates T = inter (op =) (filter restriction (T :: styps sup T));
in