# HG changeset patch
# User wenzelm
# Date 1445113881 -7200
# Node ID 9a468c3a1fa10415248fc55c9fc9efdb441029f8
# Parent  79900ab5d50a5bd4c8ef76e7dcd4437c0fc8113e
tuned signature;

diff -r 79900ab5d50a -r 9a468c3a1fa1 src/HOL/HOLCF/Tools/Domain/domain.ML
--- a/src/HOL/HOLCF/Tools/Domain/domain.ML	Sat Oct 17 21:42:18 2015 +0200
+++ b/src/HOL/HOLCF/Tools/Domain/domain.ML	Sat Oct 17 22:31:21 2015 +0200
@@ -229,7 +229,7 @@
 
 val dest_decl : (bool * binding option * string) parser =
   @{keyword "("} |-- Scan.optional (@{keyword "lazy"} >> K true) false --
-    (Parse.binding >> SOME) -- (@{keyword "::"} |-- Parse.typ)  --| @{keyword ")"} >> Parse.triple1
+    (Parse.binding >> SOME) -- (@{keyword "::"} |-- Parse.typ)  --| @{keyword ")"} >> Scan.triple1
     || @{keyword "("} |-- @{keyword "lazy"} |-- Parse.typ --| @{keyword ")"}
     >> (fn t => (true, NONE, t))
     || Parse.typ >> (fn t => (false, NONE, t))
diff -r 79900ab5d50a -r 9a468c3a1fa1 src/HOL/Library/old_recdef.ML
--- a/src/HOL/Library/old_recdef.ML	Sat Oct 17 21:42:18 2015 +0200
+++ b/src/HOL/Library/old_recdef.ML	Sat Oct 17 22:31:21 2015 +0200
@@ -2881,7 +2881,8 @@
     (@{keyword "("} -- Parse.!!! (@{keyword "permissive"} -- @{keyword ")"}) >> K false) true --
   Parse.name -- Parse.term -- Scan.repeat1 (Parse_Spec.opt_thm_name ":" -- Parse.prop)
     -- Scan.option hints
-  >> (fn ((((p, f), R), eqs), src) => #1 o add_recdef p f R (map Parse.triple_swap eqs) src);
+  >> (fn ((((p, f), R), eqs), src) =>
+      #1 o add_recdef p f R (map (fn ((x, y), z) => ((x, z), y)) eqs) src);
 
 val _ =
   Outer_Syntax.command @{command_keyword recdef} "define general recursive functions (obsolete TFL)"
diff -r 79900ab5d50a -r 9a468c3a1fa1 src/HOL/Tools/Lifting/lifting_def_code_dt.ML
--- a/src/HOL/Tools/Lifting/lifting_def_code_dt.ML	Sat Oct 17 21:42:18 2015 +0200
+++ b/src/HOL/Tools/Lifting/lifting_def_code_dt.ML	Sat Oct 17 22:31:21 2015 +0200
@@ -810,9 +810,9 @@
     "definition for constants over the quotient type"
     (parse_params --
       (((Parse.binding -- (@{keyword "::"} |-- (Parse.typ >> SOME) -- Parse.opt_mixfix')
-          >> Parse.triple2) --
+          >> Scan.triple2) --
         (@{keyword "is"} |-- Parse.term) --
-        Scan.optional (@{keyword "parametric"} |-- Parse.!!! Parse.xthms1) []) >> Parse.triple1)
+        Scan.optional (@{keyword "parametric"} |-- Parse.!!! Parse.xthms1) []) >> Scan.triple1)
      >> lift_def_cmd_with_err_handling);
 
 end
diff -r 79900ab5d50a -r 9a468c3a1fa1 src/HOL/Tools/Old_Datatype/old_datatype.ML
--- a/src/HOL/Tools/Old_Datatype/old_datatype.ML	Sat Oct 17 21:42:18 2015 +0200
+++ b/src/HOL/Tools/Old_Datatype/old_datatype.ML	Sat Oct 17 22:31:21 2015 +0200
@@ -800,7 +800,7 @@
 val spec_cmd =
   Parse.type_args_constrained -- Parse.binding -- Parse.opt_mixfix --
   (@{keyword "="} |-- Parse.enum1 "|" (Parse.binding -- Scan.repeat Parse.typ -- Parse.opt_mixfix))
-  >> (fn (((vs, t), mx), cons) => ((t, vs, mx), map Parse.triple1 cons));
+  >> (fn (((vs, t), mx), cons) => ((t, vs, mx), map Scan.triple1 cons));
 
 val _ =
   Outer_Syntax.command @{command_keyword old_datatype} "define old-style inductive datatypes"
diff -r 79900ab5d50a -r 9a468c3a1fa1 src/HOL/Tools/SMT/z3_replay_methods.ML
--- a/src/HOL/Tools/SMT/z3_replay_methods.ML	Sat Oct 17 21:42:18 2015 +0200
+++ b/src/HOL/Tools/SMT/z3_replay_methods.ML	Sat Oct 17 22:31:21 2015 +0200
@@ -209,7 +209,7 @@
 fun abstract_bin abs f t t1 t2 = abstract_sub t (abs t1 ##>> abs t2 #>> f)
 
 fun abstract_ter abs f t t1 t2 t3 =
-  abstract_sub t (abs t1 ##>> abs t2 ##>> abs t3 #>> (Parse.triple1 #> f))
+  abstract_sub t (abs t1 ##>> abs t2 ##>> abs t3 #>> (Scan.triple1 #> f))
 
 fun abstract_lit (@{const HOL.Not} $ t) = abstract_term t #>> HOLogic.mk_not
   | abstract_lit t = abstract_term t
diff -r 79900ab5d50a -r 9a468c3a1fa1 src/Pure/General/scan.ML
--- a/src/Pure/General/scan.ML	Sat Oct 17 21:42:18 2015 +0200
+++ b/src/Pure/General/scan.ML	Sat Oct 17 22:31:21 2015 +0200
@@ -42,6 +42,8 @@
   val error: ('a -> 'b) -> 'a -> 'b
   val catch: ('a -> 'b) -> 'a -> 'b    (*exception Fail*)
   val recover: ('a -> 'b) -> (string -> 'a -> 'b) -> 'a -> 'b
+  val triple1: ('a * 'b) * 'c -> 'a * 'b * 'c
+  val triple2: 'a * ('b * 'c) -> 'a * 'b * 'c
   val fail: 'a -> 'b
   val fail_with: ('a -> message) -> 'a -> 'b
   val succeed: 'a -> 'b -> 'a * 'b
@@ -115,6 +117,12 @@
   catch scan1 xs handle Fail msg => scan2 msg xs;
 
 
+(* utils *)
+
+fun triple1 ((x, y), z) = (x, y, z);
+fun triple2 (x, (y, z)) = (x, y, z);
+
+
 (* scanner combinators *)
 
 fun (scan >> f) xs = scan xs |>> f;
diff -r 79900ab5d50a -r 9a468c3a1fa1 src/Pure/Isar/isar_syn.ML
--- a/src/Pure/Isar/isar_syn.ML	Sat Oct 17 21:42:18 2015 +0200
+++ b/src/Pure/Isar/isar_syn.ML	Sat Oct 17 22:31:21 2015 +0200
@@ -466,7 +466,7 @@
   Outer_Syntax.command @{command_keyword overloading} "overloaded definitions"
    (Scan.repeat1 (Parse.name --| (@{keyword "\<equiv>"} || @{keyword "=="}) -- Parse.term --
       Scan.optional (@{keyword "("} |-- (@{keyword "unchecked"} >> K false) --| @{keyword ")"}) true
-      >> Parse.triple1) --| Parse.begin
+      >> Scan.triple1) --| Parse.begin
    >> (fn operations => Toplevel.begin_local_theory true (Overloading.overloading_cmd operations)));
 
 
diff -r 79900ab5d50a -r 9a468c3a1fa1 src/Pure/Isar/parse.ML
--- a/src/Pure/Isar/parse.ML	Sat Oct 17 21:42:18 2015 +0200
+++ b/src/Pure/Isar/parse.ML	Sat Oct 17 22:31:21 2015 +0200
@@ -9,9 +9,6 @@
   val group: (unit -> string) -> (Token.T list -> 'a) -> Token.T list -> 'a
   val !!! : (Token.T list -> 'a) -> Token.T list -> 'a
   val !!!! : (Token.T list -> 'a) -> Token.T list -> 'a
-  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
   val not_eof: Token.T parser
   val token: 'a parser -> Token.T parser
   val range: 'a parser -> ('a * Position.range) parser
@@ -160,13 +157,6 @@
 
 (** basic parsers **)
 
-(* utils *)
-
-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 *)
 
 fun RESET_VALUE atom = (*required for all primitive parsers*)
@@ -300,10 +290,10 @@
 val type_const = inner_syntax (group (fn () => "type constructor") xname);
 
 val arity = type_const -- ($$$ "::" |-- !!!
-  (Scan.optional ($$$ "(" |-- !!! (list1 sort --| $$$ ")")) [] -- sort)) >> triple2;
+  (Scan.optional ($$$ "(" |-- !!! (list1 sort --| $$$ ")")) [] -- sort)) >> Scan.triple2;
 
 val multi_arity = and_list1 type_const -- ($$$ "::" |-- !!!
-  (Scan.optional ($$$ "(" |-- !!! (list1 sort --| $$$ ")")) [] -- sort)) >> triple2;
+  (Scan.optional ($$$ "(" |-- !!! (list1 sort --| $$$ ")")) [] -- sort)) >> Scan.triple2;
 
 
 (* types *)
@@ -329,7 +319,7 @@
 
 val mfix = string --
   !!! (Scan.optional ($$$ "[" |-- !!! (list nat --| $$$ "]")) [] --
-    Scan.optional nat 1000) >> (Mixfix o triple2);
+    Scan.optional nat 1000) >> (Mixfix o Scan.triple2);
 
 val infx = $$$ "infix" |-- !!! (string -- nat >> Infix);
 val infxl = $$$ "infixl" |-- !!! (string -- nat >> Infixl);
@@ -338,7 +328,7 @@
 
 val binder = $$$ "binder" |--
   !!! (string -- ($$$ "[" |-- nat --| $$$ "]" -- nat || nat >> (fn n => (n, n))))
-  >> (Binder o triple2);
+  >> (Binder o Scan.triple2);
 
 val mixfix_body = mfix || strcture || binder || infxl || infxr || infx;
 
@@ -359,10 +349,10 @@
 
 val where_ = $$$ "where";
 
-val const_decl = name -- ($$$ "::" |-- !!! typ) -- opt_mixfix >> triple1;
-val const_binding = binding -- ($$$ "::" |-- !!! typ) -- opt_mixfix >> triple1;
+val const_decl = name -- ($$$ "::" |-- !!! typ) -- opt_mixfix >> Scan.triple1;
+val const_binding = binding -- ($$$ "::" |-- !!! typ) -- opt_mixfix >> Scan.triple1;
 
-val param_mixfix = binding -- Scan.option ($$$ "::" |-- typ) -- mixfix' >> (single o triple1);
+val param_mixfix = binding -- Scan.option ($$$ "::" |-- typ) -- mixfix' >> (single o Scan.triple1);
 val params =
   Scan.repeat1 binding -- Scan.option ($$$ "::" |-- !!! typ)
     >> (fn (xs, T) => map (fn x => (x, T, NoSyn)) xs);
diff -r 79900ab5d50a -r 9a468c3a1fa1 src/Pure/Isar/parse_spec.ML
--- a/src/Pure/Isar/parse_spec.ML	Sat Oct 17 21:42:18 2015 +0200
+++ b/src/Pure/Isar/parse_spec.ML	Sat Oct 17 22:31:21 2015 +0200
@@ -63,7 +63,7 @@
     (Parse.where_ >> K (NONE, NoSyn) ||
       Parse.$$$ "::" |-- Parse.!!! ((Parse.typ >> SOME) -- Parse.opt_mixfix' --| Parse.where_) ||
       Scan.ahead (Parse.$$$ "(") |-- Parse.!!! (Parse.mixfix' --| Parse.where_ >> pair NONE))
-  >> Parse.triple2;
+  >> Scan.triple2;
 
 val constdef = Scan.option constdecl -- (opt_thm_name ":" -- Parse.prop);
 
@@ -74,7 +74,7 @@
 
 val locale_fixes =
   Parse.and_list1 (Parse.binding -- Scan.option (Parse.$$$ "::" |-- Parse.typ) -- Parse.mixfix
-    >> (single o Parse.triple1) ||
+    >> (single o Scan.triple1) ||
   Parse.params) >> flat;
 
 val locale_insts =
diff -r 79900ab5d50a -r 9a468c3a1fa1 src/ZF/Tools/datatype_package.ML
--- a/src/ZF/Tools/datatype_package.ML	Sat Oct 17 21:42:18 2015 +0200
+++ b/src/ZF/Tools/datatype_package.ML	Sat Oct 17 22:31:21 2015 +0200
@@ -423,7 +423,7 @@
 
 val con_decl =
   Parse.name -- Scan.optional (@{keyword "("} |-- Parse.list1 Parse.term --| @{keyword ")"}) [] --
-    Parse.opt_mixfix >> Parse.triple1;
+    Parse.opt_mixfix >> Scan.triple1;
 
 val coind_prefix = if coind then "co" else "";
 
diff -r 79900ab5d50a -r 9a468c3a1fa1 src/ZF/Tools/inductive_package.ML
--- a/src/ZF/Tools/inductive_package.ML	Sat Oct 17 21:42:18 2015 +0200
+++ b/src/ZF/Tools/inductive_package.ML	Sat Oct 17 22:31:21 2015 +0200
@@ -579,7 +579,8 @@
 (* outer syntax *)
 
 fun mk_ind (((((doms, intrs), monos), con_defs), type_intrs), type_elims) =
-  #1 o add_inductive doms (map Parse.triple_swap intrs) (monos, con_defs, type_intrs, type_elims);
+  #1 o add_inductive doms (map (fn ((x, y), z) => ((x, z), y)) intrs)
+    (monos, con_defs, type_intrs, type_elims);
 
 val ind_decl =
   (@{keyword "domains"} |-- Parse.!!! (Parse.enum1 "+" Parse.term --
diff -r 79900ab5d50a -r 9a468c3a1fa1 src/ZF/Tools/primrec_package.ML
--- a/src/ZF/Tools/primrec_package.ML	Sat Oct 17 21:42:18 2015 +0200
+++ b/src/ZF/Tools/primrec_package.ML	Sat Oct 17 22:31:21 2015 +0200
@@ -199,7 +199,7 @@
 val _ =
   Outer_Syntax.command @{command_keyword primrec} "define primitive recursive functions on datatypes"
     (Scan.repeat1 (Parse_Spec.opt_thm_name ":" -- Parse.prop)
-      >> (Toplevel.theory o (#1 oo (primrec o map Parse.triple_swap))));
+      >> (Toplevel.theory o (#1 oo (primrec o map (fn ((x, y), z) => ((x, z), y))))));
 
 end;