changeset 33040 | cffdb7b28498 |
parent 32966 | 5b21661fe618 |
--- a/src/HOL/Tools/Function/fundef_common.ML Wed Oct 21 08:16:25 2009 +0200 +++ b/src/HOL/Tools/Function/fundef_common.ML Wed Oct 21 10:15:31 2009 +0200 @@ -234,7 +234,7 @@ val _ = length args > 0 orelse input_error "Function has no arguments:" fun add_bvs t is = add_loose_bnos (t, 0, is) - val rvs = (add_bvs rhs [] \\ fold add_bvs args []) + val rvs = (subtract (op =) (fold add_bvs args []) (add_bvs rhs [])) |> map (fst o nth (rev qs)) val _ = null rvs orelse input_error