src/Pure/type_infer.ML
changeset 42386 50ea65e84d98
parent 42383 0ae4ad40d7b5
child 42400 26c8c9cabb24
     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