changeset 42793 | 88bee9f6eec7 |
parent 42361 | 23f352990944 |
child 42947 | fcb6250bf6b4 |
--- a/src/HOL/Tools/Function/fun.ML Fri May 13 16:03:03 2011 +0200 +++ b/src/HOL/Tools/Function/fun.ML Fri May 13 22:55:00 2011 +0200 @@ -143,7 +143,7 @@ let fun pat_completeness_auto ctxt = Pat_Completeness.pat_completeness_tac ctxt 1 - THEN auto_tac (clasimpset_of ctxt) + THEN auto_tac ctxt fun prove_termination lthy = Function.prove_termination NONE (Function_Common.get_termination_prover lthy lthy) lthy