src/ZF/Fin.ML

 Fin(univ(A)) <= univ(A)
 *)
 
 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)"]
   val monos      = []
   val con_defs   = []
   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;
 
 
 goalw Fin.thy Fin.defs "!!A B. A<=B ==> Fin(A) <= Fin(B)";