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/Datatype/datatype_prop.ML
changeset 46218 ecf6375e2abb
parent 46215 0da9433f959e
child 46219 426ed18eba43 
--- a/src/HOL/Tools/Datatype/datatype_prop.ML	Sat Jan 14 19:06:05 2012 +0100
+++ b/src/HOL/Tools/Datatype/datatype_prop.ML	Sat Jan 14 20:05:58 2012 +0100
@@ -125,7 +125,7 @@
         fun mk_prem ((dt, s), T) =
           let val (Us, U) = strip_type T
           in
-            list_all (map (pair "x") Us,
+            Logic.list_all (map (pair "x") Us,
               HOLogic.mk_Trueprop
                 (make_pred (Datatype_Aux.body_index dt) U $
                   Datatype_Aux.app_bnds (Free (s, T)) (length Us)))
isabelle