# HG changeset patch
# User bulwahn
# Date 1321367929 -3600
# Node ID 4cc83e901acf35ea5f9f587b2596f40b1df42dcf
# Parent  dc452a1a46e55e133e6f7389ddd8420d80c5005f
tuned

diff -r dc452a1a46e5 -r 4cc83e901acf src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML
--- a/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML	Tue Nov 15 12:51:14 2011 +0100
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML	Tue Nov 15 15:38:49 2011 +0100
@@ -982,7 +982,6 @@
       | is_param_type T = is_some (try (dest_monadT compfuns) T)
     val (inpTs, outTs) = split_map_modeT (fn m => fn T => (SOME (funT_of compfuns m T), NONE)) mode
       (binder_types T)
-    val predT = mk_monadT compfuns (HOLogic.mk_tupleT outTs)
     val funT = Comp_Mod.funT_of compilation_modifiers mode T
     val (in_ts, _) = fold_map (fold_map_aterms_prodT (curry HOLogic.mk_prod)
       (fn T => fn (param_vs, names) =>