proper local Proof_Context.arity_sorts;
authorwenzelm
Sun Mar 29 19:23:08 2015 +0200 (2015-03-29)
changeset 598400ab8750c9342
parent 59839 62d69ffa639f
child 59841 2551ac44150e
proper local Proof_Context.arity_sorts;
src/Pure/Isar/proof_context.ML
src/Pure/type_infer_context.ML
src/Tools/Code/code_preproc.ML
src/Tools/subtyping.ML
     1.1 --- a/src/Pure/Isar/proof_context.ML	Sun Mar 29 18:32:28 2015 +0200
     1.2 +++ b/src/Pure/Isar/proof_context.ML	Sun Mar 29 19:23:08 2015 +0200
     1.3 @@ -26,6 +26,7 @@
     1.4    val tsig_of: Proof.context -> Type.tsig
     1.5    val set_defsort: sort -> Proof.context -> Proof.context
     1.6    val default_sort: Proof.context -> indexname -> sort
     1.7 +  val arity_sorts: Proof.context -> string -> sort -> sort list
     1.8    val consts_of: Proof.context -> Consts.T
     1.9    val set_syntax_mode: Syntax.mode -> Proof.context -> Proof.context
    1.10    val restore_syntax_mode: Proof.context -> Proof.context -> Proof.context
    1.11 @@ -289,6 +290,7 @@
    1.12  val tsig_of = #1 o #tsig o rep_data;
    1.13  val set_defsort = map_tsig o apfst o Type.set_defsort;
    1.14  fun default_sort ctxt = the_default (Type.defaultS (tsig_of ctxt)) o Variable.def_sort ctxt;
    1.15 +fun arity_sorts ctxt = Type.arity_sorts (Context.pretty ctxt) (tsig_of ctxt);
    1.16  
    1.17  val consts_of = #1 o #consts o rep_data;
    1.18  val cases_of = #cases o rep_data;
     2.1 --- a/src/Pure/type_infer_context.ML	Sun Mar 29 18:32:28 2015 +0200
     2.2 +++ b/src/Pure/type_infer_context.ML	Sun Mar 29 19:23:08 2015 +0200
     2.3 @@ -169,7 +169,7 @@
     2.4  fun unify ctxt =
     2.5    let
     2.6      val thy = Proof_Context.theory_of ctxt;
     2.7 -    val arity_sorts = Type.arity_sorts (Context.pretty ctxt) (Sign.tsig_of thy);
     2.8 +    val arity_sorts = Proof_Context.arity_sorts ctxt;
     2.9  
    2.10  
    2.11      (* adjust sorts of parameters *)
     3.1 --- a/src/Tools/Code/code_preproc.ML	Sun Mar 29 18:32:28 2015 +0200
     3.2 +++ b/src/Tools/Code/code_preproc.ML	Sun Mar 29 19:23:08 2015 +0200
     3.3 @@ -371,8 +371,9 @@
     3.4          val thy = Proof_Context.theory_of ctxt;
     3.5          val all_classes = complete_proper_sort thy [class];
     3.6          val super_classes = remove (op =) class all_classes;
     3.7 -        val classess = map (complete_proper_sort thy)
     3.8 -          (Sign.arity_sorts thy tyco [class]);
     3.9 +        val classess =
    3.10 +          map (complete_proper_sort thy)
    3.11 +            (Proof_Context.arity_sorts ctxt tyco [class]);
    3.12          val inst_params = inst_params thy tyco all_classes;
    3.13        in (classess, (super_classes, inst_params)) end;
    3.14  
    3.15 @@ -410,7 +411,7 @@
    3.16      |> apfst (Vargraph.add_edge (c_k, c_k'))
    3.17    end
    3.18  and ensure_typmatch_inst ctxt arities eqngr (tyco, styps) class vardeps_data =
    3.19 -  if can (Sign.arity_sorts (Proof_Context.theory_of ctxt) tyco) [class]
    3.20 +  if can (Proof_Context.arity_sorts ctxt tyco) [class]
    3.21    then vardeps_data
    3.22      |> ensure_inst ctxt arities eqngr (class, tyco)
    3.23      |> fold_index (fn (k, styp) =>
     4.1 --- a/src/Tools/subtyping.ML	Sun Mar 29 18:32:28 2015 +0200
     4.2 +++ b/src/Tools/subtyping.ML	Sun Mar 29 19:23:08 2015 +0200
     4.3 @@ -144,7 +144,7 @@
     4.4  fun unify weak ctxt =
     4.5    let
     4.6      val thy = Proof_Context.theory_of ctxt;
     4.7 -    val arity_sorts = Type.arity_sorts (Context.pretty ctxt) (Sign.tsig_of thy);
     4.8 +    val arity_sorts = Proof_Context.arity_sorts ctxt;
     4.9  
    4.10  
    4.11      (* adjust sorts of parameters *)
    4.12 @@ -344,7 +344,7 @@
    4.13  
    4.14      val coes_graph = coes_graph_of ctxt;
    4.15      val tmaps = tmaps_of ctxt;
    4.16 -    val arity_sorts = Type.arity_sorts (Context.pretty ctxt) (Sign.tsig_of thy);
    4.17 +    val arity_sorts = Proof_Context.arity_sorts ctxt;
    4.18  
    4.19      fun split_cs _ [] = ([], [])
    4.20        | split_cs f (c :: cs) =