# HG changeset patch
# User wenzelm
# Date 1391453416 -3600
# Node ID 70e7ac6af16f70e010383390ac2d0bbfbfa1c667
# Parent  55ac31bc08a48fac57bc07a361e8b295da4a911b
unused;

diff -r 55ac31bc08a4 -r 70e7ac6af16f src/Tools/subtyping.ML
--- a/src/Tools/subtyping.ML	Mon Feb 03 16:33:54 2014 +0100
+++ b/src/Tools/subtyping.ML	Mon Feb 03 19:50:16 2014 +0100
@@ -71,14 +71,6 @@
   Data.map (fn Data {coes, full_graph, coes_graph, tmaps, coerce_args} =>
     make_data (f (coes, full_graph, coes_graph, tmaps, coerce_args)));
 
-fun map_coes f =
-  map_data (fn (coes, full_graph, coes_graph, tmaps, coerce_args) =>
-    (f coes, full_graph, coes_graph, tmaps, coerce_args));
-
-fun map_coes_graph f =
-  map_data (fn (coes, full_graph, coes_graph, tmaps, coerce_args) =>
-    (coes, full_graph, f coes_graph, tmaps, coerce_args));
-
 fun map_coes_and_graphs f =
   map_data (fn (coes, full_graph, coes_graph, tmaps, coerce_args) =>
     let val (coes', full_graph', coes_graph') = f (coes, full_graph, coes_graph);
@@ -113,7 +105,6 @@
   | sort_of _ = NONE;
 
 val is_typeT = fn (Type _) => true | _ => false;
-val is_stypeT = fn (Type (_, [])) => true | _ => false;
 val is_compT = fn (Type (_, _ :: _)) => true | _ => false;
 val is_freeT = fn (TFree _) => true | _ => false;
 val is_fixedvarT = fn (TVar (xi, _)) => not (Type_Infer.is_param xi) | _ => false;
@@ -929,7 +920,7 @@
               else error ("Functions do not apply to arguments correctly:" ^ err_str t));
 
     (*retry flag needed to adjust the type lists, when given a map over type constructor fun*)
-    fun check_map_fun fis (Type (C1, Ts)) (Type (C2, Us)) retry =
+    fun check_map_fun fis (Type (C1, Ts)) (Type (C2, Us)) _ =
           if C1 = C2 andalso not (null fis) andalso forall is_funtype fis
           then ((map dest_funT fis, Ts ~~ Us), C1)
           else error ("Not a proper map function:" ^ err_str t)