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.ML
changeset 46218 ecf6375e2abb
parent 45910 566c34b64f70
child 46219 426ed18eba43 
--- a/src/HOL/Tools/Datatype/datatype.ML	Sat Jan 14 19:06:05 2012 +0100
+++ b/src/HOL/Tools/Datatype/datatype.ML	Sat Jan 14 20:05:58 2012 +0100
@@ -156,7 +156,7 @@
                 val free_t =
                   Datatype_Aux.app_bnds (Datatype_Aux.mk_Free "x" (Ts ---> Univ_elT) j) (length Ts)
               in
-                (j + 1, list_all (map (pair "x") Ts,
+                (j + 1, Logic.list_all (map (pair "x") Ts,
                   HOLogic.mk_Trueprop
                     (Free (nth rep_set_names' k, UnivT') $ free_t)) :: prems,
                 mk_lim free_t Ts :: ts)
isabelle