src/HOLCF/Tools/Domain/domain_extender.ML

     val dtnvs' =
       map (fn (dname,vs,mx) => (Sign.full_name thy dname,vs)) dtnvs;
     val eqs' : ((string * typ list) *
         (binding * (bool * binding option * typ) list * mixfix) list) list =
       check_and_sort_domain false dtnvs' cons'' thy;
-    val thy = thy |> Domain_Syntax.add_syntax false eqs';
+    val thy = Domain_Syntax.add_syntax eqs' thy;
     val dts  = map (Type o fst) eqs';
     val new_dts = map (fn ((s,Ts),_) => (s, map (fst o dest_TFree) Ts)) eqs';
     fun strip ss = drop (find_index (fn s => s = "'") ss + 1) ss;
     fun one_con (con,args,mx) =
         (Binding.name_of con,  (* FIXME preverse binding (!?) *)

       Domain_Isomorphism.domain_isomorphism
         (map (fn ((vs, dname, mx, _), eq) =>
                  (map fst vs, dname, mx, mk_eq_typ eq, NONE))
              (eqs''' ~~ eqs'))
 
-    val thy = thy |> Domain_Syntax.add_syntax true eqs';
     val dts  = map (Type o fst) eqs';
     val new_dts = map (fn ((s,Ts),_) => (s, map (fst o dest_TFree) Ts)) eqs';
     fun strip ss = drop (find_index (fn s => s = "'") ss + 1) ss;
     fun one_con (con,args,mx) =
         (Binding.name_of con,   (* FIXME preverse binding (!?) *)