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/List.thy
changeset 22994 02440636214f
parent 22940 42de50e78446
child 23029 79ee75dc1e59 
--- a/src/HOL/List.thy	Thu May 17 19:49:16 2007 +0200
+++ b/src/HOL/List.thy	Thu May 17 19:49:17 2007 +0200
@@ -320,7 +320,7 @@
     fun prove_neq() =
       let
         val Type(_,listT::_) = eqT;
-        val size = Const("Nat.size", listT --> HOLogic.natT);
+        val size = HOLogic.size_const listT;
         val eq_len = HOLogic.mk_eq (size $ lhs, size $ rhs);
         val neq_len = HOLogic.mk_Trueprop (HOLogic.Not $ eq_len);
         val thm = Goal.prove (Simplifier.the_context ss) [] [] neq_len
isabelle