src/ZF/Fin.ML

--- a/src/ZF/Fin.ML	Wed Jun 29 12:13:03 1994 +0200
+++ b/src/ZF/Fin.ML	Fri Jul 01 11:03:42 1994 +0200
@@ -16,7 +16,7 @@
 *)
 
 structure Fin = Inductive_Fun
- (val thy        = Arith.thy addconsts [(["Fin"],"i=>i")]
+ (val thy        = Arith.thy |> add_consts [("Fin", "i=>i", NoSyn)]
   val rec_doms   = [("Fin","Pow(A)")]
   val sintrs     = ["0 : Fin(A)",
                     "[| a: A;  b: Fin(A) |] ==> cons(a,b) : Fin(A)"]