changeset 25545 | 21cd20c1ce98 |
parent 22733 | 0b14bb35be90 |
child 30510 | 4120fc59dd85 |
--- a/src/HOL/Tools/function_package/auto_term.ML Wed Dec 05 14:32:17 2007 +0100 +++ b/src/HOL/Tools/function_package/auto_term.ML Wed Dec 05 14:36:58 2007 +0100 @@ -26,7 +26,7 @@ end fun relation_tac ctxt rel i = - FundefCommon.apply_termination_rule ctxt i + TRY (FundefCommon.apply_termination_rule ctxt i) THEN PRIMITIVE (inst_thm ctxt rel) val setup = Method.add_methods