src/ZF/ex/Acc.ML

--- a/src/ZF/ex/Acc.ML	Fri Jul 01 11:03:42 1994 +0200
+++ b/src/ZF/ex/Acc.ML	Fri Jul 01 11:04:12 1994 +0200
@@ -10,7 +10,7 @@
 *)
 
 structure Acc = Inductive_Fun
- (val thy        = WF.thy addconsts [(["acc"],"i=>i")]
+ (val thy        = WF.thy |> add_consts [("acc","i=>i",NoSyn)]
   val rec_doms   = [("acc", "field(r)")]
   val sintrs     = ["[| r-``{a}: Pow(acc(r)); a: field(r) |] ==> a: acc(r)"]
   val monos      = [Pow_mono]