# HG changeset patch
# User wenzelm
# Date 1427649788 -7200
# Node ID 0ab8750c9342af6f45304f0964f7c008ba4d95c3
# Parent  62d69ffa639fe46197b47b16008c0188270b3495
proper local Proof_Context.arity_sorts;

diff -r 62d69ffa639f -r 0ab8750c9342 src/Pure/Isar/proof_context.ML
--- a/src/Pure/Isar/proof_context.ML	Sun Mar 29 18:32:28 2015 +0200
+++ b/src/Pure/Isar/proof_context.ML	Sun Mar 29 19:23:08 2015 +0200
@@ -26,6 +26,7 @@
   val tsig_of: Proof.context -> Type.tsig
   val set_defsort: sort -> Proof.context -> Proof.context
   val default_sort: Proof.context -> indexname -> sort
+  val arity_sorts: Proof.context -> string -> sort -> sort list
   val consts_of: Proof.context -> Consts.T
   val set_syntax_mode: Syntax.mode -> Proof.context -> Proof.context
   val restore_syntax_mode: Proof.context -> Proof.context -> Proof.context
@@ -289,6 +290,7 @@
 val tsig_of = #1 o #tsig o rep_data;
 val set_defsort = map_tsig o apfst o Type.set_defsort;
 fun default_sort ctxt = the_default (Type.defaultS (tsig_of ctxt)) o Variable.def_sort ctxt;
+fun arity_sorts ctxt = Type.arity_sorts (Context.pretty ctxt) (tsig_of ctxt);
 
 val consts_of = #1 o #consts o rep_data;
 val cases_of = #cases o rep_data;
diff -r 62d69ffa639f -r 0ab8750c9342 src/Pure/type_infer_context.ML
--- a/src/Pure/type_infer_context.ML	Sun Mar 29 18:32:28 2015 +0200
+++ b/src/Pure/type_infer_context.ML	Sun Mar 29 19:23:08 2015 +0200
@@ -169,7 +169,7 @@
 fun unify ctxt =
   let
     val thy = Proof_Context.theory_of ctxt;
-    val arity_sorts = Type.arity_sorts (Context.pretty ctxt) (Sign.tsig_of thy);
+    val arity_sorts = Proof_Context.arity_sorts ctxt;
 
 
     (* adjust sorts of parameters *)
diff -r 62d69ffa639f -r 0ab8750c9342 src/Tools/Code/code_preproc.ML
--- a/src/Tools/Code/code_preproc.ML	Sun Mar 29 18:32:28 2015 +0200
+++ b/src/Tools/Code/code_preproc.ML	Sun Mar 29 19:23:08 2015 +0200
@@ -371,8 +371,9 @@
         val thy = Proof_Context.theory_of ctxt;
         val all_classes = complete_proper_sort thy [class];
         val super_classes = remove (op =) class all_classes;
-        val classess = map (complete_proper_sort thy)
-          (Sign.arity_sorts thy tyco [class]);
+        val classess =
+          map (complete_proper_sort thy)
+            (Proof_Context.arity_sorts ctxt tyco [class]);
         val inst_params = inst_params thy tyco all_classes;
       in (classess, (super_classes, inst_params)) end;
 
@@ -410,7 +411,7 @@
     |> apfst (Vargraph.add_edge (c_k, c_k'))
   end
 and ensure_typmatch_inst ctxt arities eqngr (tyco, styps) class vardeps_data =
-  if can (Sign.arity_sorts (Proof_Context.theory_of ctxt) tyco) [class]
+  if can (Proof_Context.arity_sorts ctxt tyco) [class]
   then vardeps_data
     |> ensure_inst ctxt arities eqngr (class, tyco)
     |> fold_index (fn (k, styp) =>
diff -r 62d69ffa639f -r 0ab8750c9342 src/Tools/subtyping.ML
--- a/src/Tools/subtyping.ML	Sun Mar 29 18:32:28 2015 +0200
+++ b/src/Tools/subtyping.ML	Sun Mar 29 19:23:08 2015 +0200
@@ -144,7 +144,7 @@
 fun unify weak ctxt =
   let
     val thy = Proof_Context.theory_of ctxt;
-    val arity_sorts = Type.arity_sorts (Context.pretty ctxt) (Sign.tsig_of thy);
+    val arity_sorts = Proof_Context.arity_sorts ctxt;
 
 
     (* adjust sorts of parameters *)
@@ -344,7 +344,7 @@
 
     val coes_graph = coes_graph_of ctxt;
     val tmaps = tmaps_of ctxt;
-    val arity_sorts = Type.arity_sorts (Context.pretty ctxt) (Sign.tsig_of thy);
+    val arity_sorts = Proof_Context.arity_sorts ctxt;
 
     fun split_cs _ [] = ([], [])
       | split_cs f (c :: cs) =