src/HOL/HOLCF/Tools/cont_consts.ML
changeset 42204 b3277168c1e7
parent 42151 4da4fc77664b
child 42224 578a51fae383
     1.1 --- a/src/HOL/HOLCF/Tools/cont_consts.ML	Sun Apr 03 18:17:21 2011 +0200
     1.2 +++ b/src/HOL/HOLCF/Tools/cont_consts.ML	Sun Apr 03 21:59:33 2011 +0200
     1.3 @@ -24,9 +24,9 @@
     1.4  fun trans_rules name2 name1 n mx =
     1.5    let
     1.6      val vnames = Name.invents Name.context "a" n
     1.7 -    val extra_parse_rule = Syntax.ParseRule (Constant name2, Constant name1)
     1.8 +    val extra_parse_rule = Syntax.Parse_Rule (Constant name2, Constant name1)
     1.9    in
    1.10 -    [Syntax.ParsePrintRule
    1.11 +    [Syntax.Parse_Print_Rule
    1.12        (Syntax.mk_appl (Constant name2) (map Variable vnames),
    1.13          fold (fn a => fn t => Syntax.mk_appl (Constant @{const_syntax Rep_cfun}) [t, Variable a])
    1.14            vnames (Constant name1))] @
    1.15 @@ -80,7 +80,7 @@
    1.16    in
    1.17      thy
    1.18      |> Sign.add_consts_i (normal_decls @ map #1 transformed_decls @ map #2 transformed_decls)
    1.19 -    |> Sign.add_trrules_i (maps #3 transformed_decls)
    1.20 +    |> Sign.add_trrules (maps #3 transformed_decls)
    1.21    end
    1.22  
    1.23  in