src/HOL/Tools/Meson/meson_clausify.ML
changeset 43324 2b47822868e4
parent 42944 9e620869a576
child 43964 9338aa218f09
     1.1 --- a/src/HOL/Tools/Meson/meson_clausify.ML	Thu Jun 09 15:38:49 2011 +0200
     1.2 +++ b/src/HOL/Tools/Meson/meson_clausify.ML	Thu Jun 09 16:34:49 2011 +0200
     1.3 @@ -75,7 +75,7 @@
     1.4          in dec_sko (subst_bound (comb, p)) (rhs :: rhss) end
     1.5        | dec_sko (Const (@{const_name All},_) $ Abs (a, T, p)) rhss =
     1.6          (*Universal quant: insert a free variable into body and continue*)
     1.7 -        let val fname = Name.variant (OldTerm.add_term_names (p,[])) a
     1.8 +        let val fname = singleton (Name.variant_list (OldTerm.add_term_names (p, []))) a
     1.9          in dec_sko (subst_bound (Free(fname,T), p)) rhss end
    1.10        | dec_sko (@{const conj} $ p $ q) rhss = rhss |> dec_sko p |> dec_sko q
    1.11        | dec_sko (@{const disj} $ p $ q) rhss = rhss |> dec_sko p |> dec_sko q