author | haftmann |
Wed, 11 Mar 2009 16:20:07 +0100 | |
changeset 30453 | 1e7e0d171653 |
parent 30452 | f00b993bda0d |
child 30454 | c816b6dcc8af |
--- a/src/HOL/Tools/hologic.ML Wed Mar 11 16:15:17 2009 +0100 +++ b/src/HOL/Tools/hologic.ML Wed Mar 11 16:20:07 2009 +0100 @@ -1,5 +1,4 @@ (* Title: HOL/hologic.ML - ID: $Id$ Author: Lawrence C Paulson and Markus Wenzel Abstract syntax operations for HOL. @@ -144,7 +143,7 @@ fun mk_set T ts = let val sT = mk_setT T; - val empty = Const ("Orderings.bot", sT); + val empty = Const ("Set.empty", sT); fun insert t u = Const ("insert", T --> sT --> sT) $ t $ u; in fold_rev insert ts empty end;