--- a/src/ZF/Fin.ML Fri Jul 15 13:30:42 1994 +0200
+++ b/src/ZF/Fin.ML Fri Jul 15 13:34:31 1994 +0200
@@ -17,6 +17,7 @@
structure Fin = Inductive_Fun
(val thy = Arith.thy |> add_consts [("Fin", "i=>i", NoSyn)]
+ val thy_name = "Fin"
val rec_doms = [("Fin","Pow(A)")]
val sintrs = ["0 : Fin(A)",
"[| a: A; b: Fin(A) |] ==> cons(a,b) : Fin(A)"]
@@ -25,8 +26,6 @@
val type_intrs = [empty_subsetI, cons_subsetI, PowI]
val type_elims = [make_elim PowD]);
-store_theory "Fin" Fin.thy;
-
val [Fin_0I, Fin_consI] = Fin.intrs;