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/Integ/IntDef.thy
changeset 20485 3078fd2eec7b
parent 20453 855f07fabd76
child 20595 db6bedfba498 
--- a/src/HOL/Integ/IntDef.thy	Wed Sep 06 10:01:27 2006 +0200
+++ b/src/HOL/Integ/IntDef.thy	Wed Sep 06 13:48:02 2006 +0200
@@ -935,7 +935,7 @@
       Type ("fun", [_, Type ("nat", [])])) $ bin) =
         SOME (Codegen.invoke_codegen thy defs s thyname b (gr,
           Const ("IntDef.nat", HOLogic.intT --> HOLogic.natT) $
-            (Const ("Numeral.number_of", HOLogic.binT --> HOLogic.intT) $ bin)))
+            (Const ("Numeral.number_of", HOLogic.intT --> HOLogic.intT) $ bin)))
   | number_of_codegen _ _ _ _ _ _ _ = NONE;
 *}
isabelle