# HG changeset patch
# User bulwahn
# Date 1319798238 -7200
# Node ID 23e1899503eea802e0ca7357c47684de7412df14
# Parent  299abd2931d5416f22a03c032f251745c5533405
removing dead code

diff -r 299abd2931d5 -r 23e1899503ee src/HOL/Tools/Predicate_Compile/mode_inference.ML
--- a/src/HOL/Tools/Predicate_Compile/mode_inference.ML	Fri Oct 28 10:33:23 2011 +0200
+++ b/src/HOL/Tools/Predicate_Compile/mode_inference.ML	Fri Oct 28 12:37:18 2011 +0200
@@ -154,17 +154,6 @@
 fun term_vTs tm =
   fold_aterms (fn Free xT => cons xT | _ => I) tm [];
 
-fun subsets i j =
-  if i <= j then
-    let
-      fun merge xs [] = xs
-        | merge [] ys = ys
-        | merge (x::xs) (y::ys) = if length x >= length y then x::merge xs (y::ys)
-            else y::merge (x::xs) ys;
-      val is = subsets (i+1) j
-    in merge (map (fn ks => i::ks) is) is end
-  else [[]];
-
 fun print_failed_mode options thy modes p (pol, m) rs is =
   if show_mode_inference options then
     let