1.1 --- a/src/HOL/Tools/Predicate_Compile/predicate_compile_aux.ML	Thu Jun 09 15:38:49 2011 +0200
     1.2 +++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_aux.ML	Thu Jun 09 16:34:49 2011 +0200
     1.3 @@ -906,7 +906,7 @@
     1.4          val Type ("fun", [T, T']) = fastype_of comb;
     1.5          val (Const (case_name, _), fs) = strip_comb comb
     1.6          val used = Term.add_tfree_names comb []
     1.7 -        val U = TFree (Name.variant used "'t", HOLogic.typeS)
     1.8 +        val U = TFree (singleton (Name.variant_list used) "'t", HOLogic.typeS)
     1.9          val x = Free ("x", T)
    1.10          val f = Free ("f", T' --> U)
    1.11          fun apply_f f' =