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/scnp_reconstruct.ML
changeset 59159 9312710451f5
parent 58819 aa43c6f05bca
child 59498 50b60f501b05 
--- a/src/HOL/Tools/Function/scnp_reconstruct.ML	Fri Dec 19 22:53:43 2014 +0100
+++ b/src/HOL/Tools/Function/scnp_reconstruct.ML	Fri Dec 19 23:01:46 2014 +0100
@@ -314,7 +314,7 @@
     end)
 
 fun gen_sizechange_tac orders autom_tac ctxt =
-  TRY (Function_Common.apply_termination_rule ctxt 1)
+  TRY (Function_Common.termination_rule_tac ctxt 1)
   THEN TRY (Termination.wf_union_tac ctxt)
   THEN (rtac @{thm wf_empty} 1 ORELSE gen_decomp_scnp_tac orders autom_tac ctxt 1)
isabelle