src/ZF/ex/Rmap.ML

--- a/src/ZF/ex/Rmap.ML	Fri Jul 01 11:03:42 1994 +0200
+++ b/src/ZF/ex/Rmap.ML	Fri Jul 01 11:04:12 1994 +0200
@@ -7,7 +7,7 @@
 *)
 
 structure Rmap = Inductive_Fun
- (val thy = List.thy addconsts [(["rmap"],"i=>i")];
+ (val thy = List.thy |> add_consts [("rmap","i=>i",NoSyn)];
   val rec_doms = [("rmap", "list(domain(r))*list(range(r))")];
   val sintrs = 
       ["<Nil,Nil> : rmap(r)",