changeset 33855 | cd8acf137c9c |
parent 33726 | 0878aecbf119 |
child 33955 | fff6f11b1f09 |
--- a/src/HOL/Tools/Function/fun.ML Mon Nov 23 13:45:16 2009 +0100 +++ b/src/HOL/Tools/Function/fun.ML Mon Nov 23 15:05:59 2009 +0100 @@ -44,7 +44,7 @@ ()) end - val (fname, qs, gs, args, rhs) = split_def ctxt geq + val (_, qs, gs, args, _) = split_def ctxt geq val _ = if not (null gs) then err "Conditional equations" else () val _ = map check_constr_pattern args