--- a/src/HOL/Tools/ctr_sugar_util.ML Tue Nov 19 14:11:26 2013 +0100
+++ b/src/HOL/Tools/ctr_sugar_util.ML Tue Nov 19 14:33:20 2013 +0100
@@ -176,9 +176,7 @@
fun rapp u t = betapply (t, u);
fun list_quant_free quant_const =
- fold_rev (fn free => fn P =>
- let val (x, T) = Term.dest_Free free;
- in quant_const T $ Term.absfree (x, T) P end);
+ fold_rev (fn Free (xT as (_, T)) => fn P => quant_const T $ Term.absfree xT P);
val list_all_free = list_quant_free HOLogic.all_const;
val list_exists_free = list_quant_free HOLogic.exists_const;