--- 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