# HG changeset patch
# User wenzelm
# Date 1379365453 -7200
# Node ID df8068269e90d513e9d681bc07c122f40e558755
# Parent  cee071d331610a9ad6b1a6977e00e0b778c40ce1
removed dead code (see also 69d4543811d0);

diff -r cee071d33161 -r df8068269e90 src/Pure/type_infer.ML
--- a/src/Pure/type_infer.ML	Mon Sep 16 19:30:33 2013 +0200
+++ b/src/Pure/type_infer.ML	Mon Sep 16 23:04:13 2013 +0200
@@ -14,7 +14,6 @@
   val mk_param: int -> sort -> typ
   val anyT: sort -> typ
   val paramify_vars: typ -> typ
-  val paramify_dummies: typ -> int -> typ * int
   val deref: typ Vartab.table -> typ -> typ
   val finish: Proof.context -> typ Vartab.table -> typ list * term list -> typ list * term list
   val fixate: Proof.context -> term list -> term list
@@ -52,18 +51,6 @@
     (Term_Subst.map_atypsT_same
       (fn TVar ((x, i), S) => (param i (x, S)) | _ => raise Same.SAME));
 
-val paramify_dummies =
-  let
-    fun dummy S maxidx = (param (maxidx + 1) ("'dummy", S), maxidx + 1);
-
-    fun paramify (TFree ("'_dummy_", S)) maxidx = dummy S maxidx
-      | paramify (Type ("dummy", _)) maxidx = dummy [] maxidx
-      | paramify (Type (a, Ts)) maxidx =
-          let val (Ts', maxidx') = fold_map paramify Ts maxidx
-          in (Type (a, Ts'), maxidx') end
-      | paramify T maxidx = (T, maxidx);
-  in paramify end;
-
 
 
 (** results **)