fixed typo
authorhaftmann
Wed, 11 Mar 2009 16:20:07 +0100
changeset 30453 1e7e0d171653
parent 30452 f00b993bda0d
child 30454 c816b6dcc8af
fixed typo
src/HOL/Tools/hologic.ML
--- 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;