--- 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;
--- 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 *)
--- 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) =>
--- 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) =