src/HOL/Tools/Predicate_Compile/predicate_compile_aux.ML
changeset 43326 47cf4bc789aa
parent 43324 2b47822868e4
child 44241 7943b69f0188
     1.1 --- a/src/HOL/Tools/Predicate_Compile/predicate_compile_aux.ML	Thu Jun 09 17:46:25 2011 +0200
     1.2 +++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_aux.ML	Thu Jun 09 17:51:49 2011 +0200
     1.3 @@ -542,7 +542,7 @@
     1.4  fun focus_ex t nctxt =
     1.5    let
     1.6      val ((xs, Ts), t') = apfst split_list (strip_ex t) 
     1.7 -    val (xs', nctxt') = Name.variants xs nctxt;
     1.8 +    val (xs', nctxt') = fold_map Name.variant xs nctxt;
     1.9      val ps' = xs' ~~ Ts;
    1.10      val vs = map Free ps';
    1.11      val t'' = Term.subst_bounds (rev vs, t');