1.1 --- a/src/HOL/Tools/Metis/metis_reconstruct.ML	Wed Aug 17 16:46:58 2011 +0200
     1.2 +++ b/src/HOL/Tools/Metis/metis_reconstruct.ML	Wed Aug 17 18:05:31 2011 +0200
     1.3 @@ -491,7 +491,7 @@
     1.4        case strip_comb flex of
     1.5          (Var (z as (_, T)), args) =>
     1.6          add_terms (Var z,
     1.7 -          fold_rev (curry absdummy) (take (length args) (binder_types T)) rigid)
     1.8 +          fold_rev absdummy (take (length args) (binder_types T)) rigid)
     1.9        | _ => I
    1.10      fun unify_potential_flex comb atom =
    1.11        if is_flex comb then unify_flex comb atom
    1.12 @@ -541,7 +541,7 @@
    1.13             if k > j then t else t $ u
    1.14           | (t, u) => t $ u)
    1.15        | repair t = t
    1.16 -    val t' = t |> repair |> fold (curry absdummy) (map snd params)
    1.17 +    val t' = t |> repair |> fold (absdummy o snd) params
    1.18      fun do_instantiate th =
    1.19        case Term.add_vars (prop_of th) []
    1.20             |> filter_out ((Meson_Clausify.is_zapped_var_name orf