triple_swap;
authorwenzelm
Wed Apr 14 19:05:28 1999 +0200 (1999-04-14)
changeset 643069400c97d3bf
parent 6429 9771ce553e56
child 6431 a42bdc45130d
triple_swap;
src/HOL/Tools/inductive_package.ML
src/HOL/Tools/primrec_package.ML
src/Pure/Isar/outer_parse.ML
     1.1 --- a/src/HOL/Tools/inductive_package.ML	Wed Apr 14 19:05:10 1999 +0200
     1.2 +++ b/src/HOL/Tools/inductive_package.ML	Wed Apr 14 19:05:28 1999 +0200
     1.3 @@ -646,7 +646,7 @@
     1.4  local open OuterParse in
     1.5  
     1.6  fun mk_ind coind (((sets, intrs), monos), con_defs) =
     1.7 -  #1 o add_inductive true coind sets (map (fn ((x, y), z) => ((x, z), y)) intrs) monos con_defs;
     1.8 +  #1 o add_inductive true coind sets (map triple_swap intrs) monos con_defs;
     1.9  
    1.10  fun ind_decl coind =
    1.11    Scan.repeat1 term --
     2.1 --- a/src/HOL/Tools/primrec_package.ML	Wed Apr 14 19:05:10 1999 +0200
     2.2 +++ b/src/HOL/Tools/primrec_package.ML	Wed Apr 14 19:05:28 1999 +0200
     2.3 @@ -270,7 +270,7 @@
     2.4  val primrecP =
     2.5    OuterSyntax.command "primrec" "define primitive recursive functions on datatypes"
     2.6      (primrec_decl >> (fn (alt_name, eqns) =>
     2.7 -      Toplevel.theory (#1 o add_primrec alt_name (map (fn ((x, y), z) => ((x, z), y)) eqns))));
     2.8 +      Toplevel.theory (#1 o add_primrec alt_name (map triple_swap eqns))));
     2.9  
    2.10  val _ = OuterSyntax.add_parsers [primrecP];
    2.11  
     3.1 --- a/src/Pure/Isar/outer_parse.ML	Wed Apr 14 19:05:10 1999 +0200
     3.2 +++ b/src/Pure/Isar/outer_parse.ML	Wed Apr 14 19:05:28 1999 +0200
     3.3 @@ -57,6 +57,7 @@
     3.4    val method: token list -> Method.text * token list
     3.5    val triple1: ('a * 'b) * 'c -> 'a * 'b * 'c
     3.6    val triple2: 'a * ('b * 'c) -> 'a * 'b * 'c
     3.7 +  val triple_swap: ('a * 'b) * 'c -> ('a * 'c) * 'b
     3.8  end;
     3.9  
    3.10  structure OuterParse: OUTER_PARSE =
    3.11 @@ -96,6 +97,7 @@
    3.12  
    3.13  fun triple1 ((x, y), z) = (x, y, z);
    3.14  fun triple2 (x, (y, z)) = (x, y, z);
    3.15 +fun triple_swap ((x, y), z) = ((x, z), y);
    3.16  
    3.17  
    3.18  (* tokens *)