# HG changeset patch
# User wenzelm
# Date 1303127543 -7200
# Node ID a44b0fdaa6c2bc62010ea8486399891a22d9a80a
# Parent  b1965c8992c84c80eb2efbb269046352842ae78c
standardized aliases of operations on tsig;

diff -r b1965c8992c8 -r a44b0fdaa6c2 src/HOL/Nominal/nominal_datatype.ML
--- 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,
diff -r b1965c8992c8 -r a44b0fdaa6c2 src/HOL/Tools/Function/partial_function.ML
--- 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
diff -r b1965c8992c8 -r a44b0fdaa6c2 src/HOL/Tools/enriched_type.ML
--- 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
diff -r b1965c8992c8 -r a44b0fdaa6c2 src/Pure/Isar/class.ML
--- 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
diff -r b1965c8992c8 -r a44b0fdaa6c2 src/Pure/Isar/overloading.ML
--- 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;
diff -r b1965c8992c8 -r a44b0fdaa6c2 src/Pure/sign.ML
--- 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;
 
 
diff -r b1965c8992c8 -r a44b0fdaa6c2 src/Tools/subtyping.ML
--- 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