equal
deleted
inserted
replaced
884 |
884 |
885 fun applied_fun_of fun_name fun_T fun_args = |
885 fun applied_fun_of fun_name fun_T fun_args = |
886 list_comb (Free (fun_name, fun_T), map Bound (length fun_args - 1 downto 0)); |
886 list_comb (Free (fun_name, fun_T), map Bound (length fun_args - 1 downto 0)); |
887 |
887 |
888 fun is_trivial_implies thm = |
888 fun is_trivial_implies thm = |
889 op aconv (Logic.dest_implies (Thm.prop_of thm)) |
889 uncurry (member (op aconv)) (Logic.strip_horn (Thm.prop_of thm)); |
890 handle TERM _ => false; |
|
891 |
890 |
892 fun add_primcorec_ursive tac_opt opts fixes specs of_specs_opt lthy = |
891 fun add_primcorec_ursive tac_opt opts fixes specs of_specs_opt lthy = |
893 let |
892 let |
894 val thy = Proof_Context.theory_of lthy; |
893 val thy = Proof_Context.theory_of lthy; |
895 |
894 |