--- a/src/HOL/HOLCF/Tools/cont_consts.ML Sun Apr 03 18:17:21 2011 +0200
+++ b/src/HOL/HOLCF/Tools/cont_consts.ML Sun Apr 03 21:59:33 2011 +0200
@@ -24,9 +24,9 @@
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))] @
@@ -80,7 +80,7 @@
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