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/termination.ML
changeset 46218 ecf6375e2abb
parent 45740 132a3e1c0fe5
child 47433 07f4bf913230 
--- a/src/HOL/Tools/Function/termination.ML	Sat Jan 14 19:06:05 2012 +0100
+++ b/src/HOL/Tools/Function/termination.ML	Sat Jan 14 20:05:58 2012 +0100
@@ -171,7 +171,7 @@
   let
     fun try rel =
       try_proof (cterm_of thy
-        (Term.list_all (vs,
+        (Logic.list_all (vs,
            Logic.mk_implies (HOLogic.mk_Trueprop Gam,
              HOLogic.mk_Trueprop (Const (rel, @{typ "nat => nat => bool"})
                $ (m2 $ r) $ (m1 $ l)))))) tac
isabelle