src/HOL/HOLCF/ex/Pattern_Match.thy
changeset 42204 b3277168c1e7
parent 42151 4da4fc77664b
child 42224 578a51fae383
     1.1 --- a/src/HOL/HOLCF/ex/Pattern_Match.thy	Sun Apr 03 18:17:21 2011 +0200
     1.2 +++ b/src/HOL/HOLCF/ex/Pattern_Match.thy	Sun Apr 03 21:59:33 2011 +0200
     1.3 @@ -516,17 +516,17 @@
     1.4            val ps = map (fn n => Variable ("p"^(string_of_int n))) ns;
     1.5            val vs = map (fn n => Variable ("v"^(string_of_int n))) ns;
     1.6          in
     1.7 -          [ParseRule (app_pat (capps (cname, xs)),
     1.8 +          [Parse_Rule (app_pat (capps (cname, xs)),
     1.9                        mk_appl pname (map app_pat xs)),
    1.10 -           ParseRule (app_var (capps (cname, xs)),
    1.11 +           Parse_Rule (app_var (capps (cname, xs)),
    1.12                        app_var (args_list xs)),
    1.13 -           PrintRule (capps (cname, ListPair.map (app "_match") (ps,vs)),
    1.14 +           Print_Rule (capps (cname, ListPair.map (app "_match") (ps,vs)),
    1.15                        app "_match" (mk_appl pname ps, args_list vs))]
    1.16          end;
    1.17        val trans_rules : Syntax.ast Syntax.trrule list =
    1.18            maps one_case_trans (pat_consts ~~ spec);
    1.19      in
    1.20 -      val thy = Sign.add_trrules_i trans_rules thy;
    1.21 +      val thy = Sign.add_trrules trans_rules thy;
    1.22      end;
    1.23  
    1.24      (* prove strictness and reduction rules of pattern combinators *)