tuned;
authorwenzelm
Mon Apr 18 12:11:58 2011 +0200 (2011-04-18)
changeset 4238650ea65e84d98
parent 42385 b46b47775cbe
child 42387 b1965c8992c8
tuned;
src/Pure/type_infer.ML
src/Tools/subtyping.ML
     1.1 --- a/src/Pure/type_infer.ML	Mon Apr 18 12:04:21 2011 +0200
     1.2 +++ b/src/Pure/type_infer.ML	Mon Apr 18 12:11:58 2011 +0200
     1.3 @@ -217,10 +217,10 @@
     1.4  
     1.5  exception NO_UNIFIER of string * typ Vartab.table;
     1.6  
     1.7 -fun unify ctxt pp =
     1.8 +fun unify ctxt =
     1.9    let
    1.10      val thy = Proof_Context.theory_of ctxt;
    1.11 -    val arity_sorts = Type.arity_sorts pp (Sign.tsig_of thy);
    1.12 +    val arity_sorts = Type.arity_sorts (Context.pretty ctxt) (Sign.tsig_of thy);
    1.13  
    1.14  
    1.15      (* adjust sorts of parameters *)
    1.16 @@ -289,9 +289,6 @@
    1.17  
    1.18  fun infer ctxt =
    1.19    let
    1.20 -    val pp = Context.pretty ctxt;
    1.21 -
    1.22 -
    1.23      (* errors *)
    1.24  
    1.25      fun prep_output tye bs ts Ts =
    1.26 @@ -328,7 +325,7 @@
    1.27              val (T, tye_idx') = inf bs t tye_idx;
    1.28              val (U, (tye, idx)) = inf bs u tye_idx';
    1.29              val V = mk_param idx [];
    1.30 -            val tye_idx'' = unify ctxt pp (U --> V, T) (tye, idx + 1)
    1.31 +            val tye_idx'' = unify ctxt (U --> V, T) (tye, idx + 1)
    1.32                handle NO_UNIFIER (msg, tye') => err_appl msg tye' bs t T u U;
    1.33            in (V, tye_idx'') end;
    1.34  
     2.1 --- a/src/Tools/subtyping.ML	Mon Apr 18 12:04:21 2011 +0200
     2.2 +++ b/src/Tools/subtyping.ML	Mon Apr 18 12:11:58 2011 +0200
     2.3 @@ -98,8 +98,7 @@
     2.4  fun unify weak ctxt =
     2.5    let
     2.6      val thy = Proof_Context.theory_of ctxt;
     2.7 -    val pp = Context.pretty ctxt;
     2.8 -    val arity_sorts = Type.arity_sorts pp (Sign.tsig_of thy);
     2.9 +    val arity_sorts = Type.arity_sorts (Context.pretty ctxt) (Sign.tsig_of thy);
    2.10  
    2.11  
    2.12      (* adjust sorts of parameters *)
    2.13 @@ -280,8 +279,7 @@
    2.14      val coes_graph = coes_graph_of ctxt;
    2.15      val tmaps = tmaps_of ctxt;
    2.16      val tsig = Sign.tsig_of (Proof_Context.theory_of ctxt);
    2.17 -    val pp = Context.pretty ctxt;
    2.18 -    val arity_sorts = Type.arity_sorts pp tsig;
    2.19 +    val arity_sorts = Type.arity_sorts (Context.pretty ctxt) tsig;
    2.20      val subsort = Type.subsort tsig;
    2.21  
    2.22      fun split_cs _ [] = ([], [])