src/HOL/HOLCF/Tools/cont_consts.ML

   | change_arrow _ T = raise TYPE ("cont_consts: change_arrow", [T], [])
 
 fun trans_rules name2 name1 n mx =
   let
     val vnames = Name.invents Name.context "a" n
-    val extra_parse_rule = Syntax.ParseRule (Constant name2, Constant name1)
+    val extra_parse_rule = Syntax.Parse_Rule (Constant name2, Constant name1)
   in
-    [Syntax.ParsePrintRule
+    [Syntax.Parse_Print_Rule
       (Syntax.mk_appl (Constant name2) (map Variable vnames),
         fold (fn a => fn t => Syntax.mk_appl (Constant @{const_syntax Rep_cfun}) [t, Variable a])
           vnames (Constant name1))] @
     (case mx of
       Infix _ => [extra_parse_rule]

     val (contconst_decls, normal_decls) = List.partition is_contconst decls
     val transformed_decls = map (transform thy) contconst_decls
   in
     thy
     |> Sign.add_consts_i (normal_decls @ map #1 transformed_decls @ map #2 transformed_decls)
-    |> Sign.add_trrules_i (maps #3 transformed_decls)
+    |> Sign.add_trrules (maps #3 transformed_decls)
   end
 
 in
 
 val add_consts = gen_add_consts Sign.certify_typ