1.1 --- a/src/Tools/misc_legacy.ML	Sat Jan 14 16:58:29 2012 +0100
     1.2 +++ b/src/Tools/misc_legacy.ML	Sat Jan 14 17:45:04 2012 +0100
     1.3 @@ -180,7 +180,7 @@
     1.4            if in_concl then (cterm u, cterm (Var ((a, i), T)))
     1.5            else (cterm u, cterm (Var ((a, i + maxidx), U)))
     1.6        (*Embed B in the original context of params and hyps*)
     1.7 -      fun embed B = list_all_free (params, Logic.list_implies (hyps, B))
     1.8 +      fun embed B = fold_rev Logic.all fparams (Logic.list_implies (hyps, B))
     1.9        (*Strip the context using elimination rules*)
    1.10        fun elim Bhyp = implies_elim_list (forall_elim_list cparams Bhyp) hypths
    1.11        (*A form of lifting that discharges assumptions.*)