--- a/src/ZF/ex/Enum.ML Fri Aug 12 11:13:23 1994 +0200
+++ b/src/ZF/ex/Enum.ML Fri Aug 12 12:28:46 1994 +0200
@@ -1,4 +1,4 @@
-(* Title: ZF/ex/enum
+(* Title: ZF/ex/Enum
ID: $Id$
Author: Lawrence C Paulson, Cambridge University Computer Laboratory
Copyright 1993 University of Cambridge
@@ -8,26 +8,9 @@
Can go up to at least 100 constructors, but it takes nearly 7 minutes...
*)
-
-(*An enumeration type with 60 contructors! -- takes about 150 seconds!*)
-fun mk_ids a 0 = []
- | mk_ids a n = a :: mk_ids (bump_string a) (n-1);
-
-val consts = mk_ids "con1" 60;
+open Enum;
-structure Enum = Datatype_Fun
- (val thy = Univ.thy;
- val thy_name = "Enum";
- val rec_specs =
- [("enum", "univ(0)",
- [(consts, "i", NoSyn)])];
- val rec_styp = "i";
- val sintrs = map (fn const => const ^ " : enum") consts;
- val monos = [];
- val type_intrs = datatype_intrs
- val type_elims = []);
-
-goal Enum.thy "con59 ~= con60";
-by (simp_tac (ZF_ss addsimps Enum.free_iffs) 1);
+goal Enum.thy "C00 ~= C01";
+by (simp_tac (ZF_ss addsimps enum.free_iffs) 1);
result();