removed dead code (see also 69d4543811d0);
authorwenzelm
Mon Sep 16 23:04:13 2013 +0200 (2013-09-16)
changeset 53672df8068269e90
parent 53671 cee071d33161
child 53673 bcfd16f65014
removed dead code (see also 69d4543811d0);
src/Pure/type_infer.ML
     1.1 --- a/src/Pure/type_infer.ML	Mon Sep 16 19:30:33 2013 +0200
     1.2 +++ b/src/Pure/type_infer.ML	Mon Sep 16 23:04:13 2013 +0200
     1.3 @@ -14,7 +14,6 @@
     1.4    val mk_param: int -> sort -> typ
     1.5    val anyT: sort -> typ
     1.6    val paramify_vars: typ -> typ
     1.7 -  val paramify_dummies: typ -> int -> typ * int
     1.8    val deref: typ Vartab.table -> typ -> typ
     1.9    val finish: Proof.context -> typ Vartab.table -> typ list * term list -> typ list * term list
    1.10    val fixate: Proof.context -> term list -> term list
    1.11 @@ -52,18 +51,6 @@
    1.12      (Term_Subst.map_atypsT_same
    1.13        (fn TVar ((x, i), S) => (param i (x, S)) | _ => raise Same.SAME));
    1.14  
    1.15 -val paramify_dummies =
    1.16 -  let
    1.17 -    fun dummy S maxidx = (param (maxidx + 1) ("'dummy", S), maxidx + 1);
    1.18 -
    1.19 -    fun paramify (TFree ("'_dummy_", S)) maxidx = dummy S maxidx
    1.20 -      | paramify (Type ("dummy", _)) maxidx = dummy [] maxidx
    1.21 -      | paramify (Type (a, Ts)) maxidx =
    1.22 -          let val (Ts', maxidx') = fold_map paramify Ts maxidx
    1.23 -          in (Type (a, Ts'), maxidx') end
    1.24 -      | paramify T maxidx = (T, maxidx);
    1.25 -  in paramify end;
    1.26 -
    1.27  
    1.28  
    1.29  (** results **)