# HG changeset patch
# User wenzelm
# Date 924109528 -7200
# Node ID 69400c97d3bf627aaf367692ab061beaea0d271b
# Parent  9771ce553e565db74e926fac8ce31dbddc228322
triple_swap;

diff -r 9771ce553e56 -r 69400c97d3bf src/HOL/Tools/inductive_package.ML
--- a/src/HOL/Tools/inductive_package.ML	Wed Apr 14 19:05:10 1999 +0200
+++ b/src/HOL/Tools/inductive_package.ML	Wed Apr 14 19:05:28 1999 +0200
@@ -646,7 +646,7 @@
 local open OuterParse in
 
 fun mk_ind coind (((sets, intrs), monos), con_defs) =
-  #1 o add_inductive true coind sets (map (fn ((x, y), z) => ((x, z), y)) intrs) monos con_defs;
+  #1 o add_inductive true coind sets (map triple_swap intrs) monos con_defs;
 
 fun ind_decl coind =
   Scan.repeat1 term --
diff -r 9771ce553e56 -r 69400c97d3bf src/HOL/Tools/primrec_package.ML
--- a/src/HOL/Tools/primrec_package.ML	Wed Apr 14 19:05:10 1999 +0200
+++ b/src/HOL/Tools/primrec_package.ML	Wed Apr 14 19:05:28 1999 +0200
@@ -270,7 +270,7 @@
 val primrecP =
   OuterSyntax.command "primrec" "define primitive recursive functions on datatypes"
     (primrec_decl >> (fn (alt_name, eqns) =>
-      Toplevel.theory (#1 o add_primrec alt_name (map (fn ((x, y), z) => ((x, z), y)) eqns))));
+      Toplevel.theory (#1 o add_primrec alt_name (map triple_swap eqns))));
 
 val _ = OuterSyntax.add_parsers [primrecP];
 
diff -r 9771ce553e56 -r 69400c97d3bf src/Pure/Isar/outer_parse.ML
--- a/src/Pure/Isar/outer_parse.ML	Wed Apr 14 19:05:10 1999 +0200
+++ b/src/Pure/Isar/outer_parse.ML	Wed Apr 14 19:05:28 1999 +0200
@@ -57,6 +57,7 @@
   val method: token list -> Method.text * token list
   val triple1: ('a * 'b) * 'c -> 'a * 'b * 'c
   val triple2: 'a * ('b * 'c) -> 'a * 'b * 'c
+  val triple_swap: ('a * 'b) * 'c -> ('a * 'c) * 'b
 end;
 
 structure OuterParse: OUTER_PARSE =
@@ -96,6 +97,7 @@
 
 fun triple1 ((x, y), z) = (x, y, z);
 fun triple2 (x, (y, z)) = (x, y, z);
+fun triple_swap ((x, y), z) = ((x, z), y);
 
 
 (* tokens *)