294 handle TERM _ => ill_formed_equation_lhs_rhs ctxt [eqn0]; |
294 handle TERM _ => ill_formed_equation_lhs_rhs ctxt [eqn0]; |
295 val (lhs, rhs) = HOLogic.dest_eq eqn |
295 val (lhs, rhs) = HOLogic.dest_eq eqn |
296 handle TERM _ => ill_formed_equation_lhs_rhs ctxt [eqn]; |
296 handle TERM _ => ill_formed_equation_lhs_rhs ctxt [eqn]; |
297 val (fun_name, args) = strip_comb lhs |
297 val (fun_name, args) = strip_comb lhs |
298 |>> (fn x => if is_Free x then fst (dest_Free x) else ill_formed_equation_head ctxt [eqn]); |
298 |>> (fn x => if is_Free x then fst (dest_Free x) else ill_formed_equation_head ctxt [eqn]); |
299 val (left_args, rest) = take_prefix is_Free args; |
299 val (left_args, rest) = chop_prefix is_Free args; |
300 val (nonfrees, right_args) = take_suffix is_Free rest; |
300 val (nonfrees, right_args) = chop_suffix is_Free rest; |
301 val num_nonfrees = length nonfrees; |
301 val num_nonfrees = length nonfrees; |
302 val _ = num_nonfrees = 1 orelse |
302 val _ = num_nonfrees = 1 orelse |
303 (if num_nonfrees = 0 then missing_pattern ctxt [eqn] |
303 (if num_nonfrees = 0 then missing_pattern ctxt [eqn] |
304 else more_than_one_nonvar_in_lhs ctxt [eqn]); |
304 else more_than_one_nonvar_in_lhs ctxt [eqn]); |
305 val _ = member (op =) fun_names fun_name orelse raise ill_formed_equation_head ctxt [eqn]; |
305 val _ = member (op =) fun_names fun_name orelse raise ill_formed_equation_head ctxt [eqn]; |