Mercurial Mercurial > repos > isabelle / diff
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/HOL/Tools/Function/fun.ML
changeset 60682 5a6cd2560549
parent 59936 b8ffc3dc9e24
child 63064 2f18172214c8 
--- a/src/HOL/Tools/Function/fun.ML	Tue Jul 07 18:01:30 2015 +0200
+++ b/src/HOL/Tools/Function/fun.ML	Tue Jul 07 18:37:24 2015 +0200
@@ -158,8 +158,7 @@
       Pat_Completeness.pat_completeness_tac ctxt 1
       THEN auto_tac ctxt
     fun prove_termination lthy =
-      Function.prove_termination NONE
-        (Function_Common.termination_prover_tac lthy) lthy
+      Function.prove_termination NONE (Function_Common.termination_prover_tac false lthy) lthy
   in
     lthy
     |> add pat_completeness_auto |> snd
isabelle