# HG changeset patch
# User wenzelm
# Date 1342385932 -7200
# Node ID fa7e99b8067530c7a40b83886dfafc0e627c902a
# Parent  429fab105d99ac1d3ac95402804624456740c2c8# Parent  94a7dc2276e4cea32b180a5bd2d4215368fc4940
merged;

diff -r 429fab105d99 -r fa7e99b80675 src/HOL/Auth/Guard/Guard_NS_Public.thy
--- a/src/HOL/Auth/Guard/Guard_NS_Public.thy	Sun Jul 15 22:56:49 2012 +0200
+++ b/src/HOL/Auth/Guard/Guard_NS_Public.thy	Sun Jul 15 22:58:52 2012 +0200
@@ -158,7 +158,10 @@
 apply (case_tac "NBa=NB", clarify)
 apply (drule Guard_Nonce_analz, simp+)
 apply (drule Says_imp_knows_Spy)+
-by (drule_tac A=Aa and A'=A in NB_is_uniq, auto)
+apply (drule_tac A=Aa and A'=A in NB_is_uniq)
+apply auto[1]
+apply (auto simp add: guard.No_Nonce)
+done
 
 subsection{*Agents' Authentication*}
 
diff -r 429fab105d99 -r fa7e99b80675 src/HOL/Auth/Guard/Guard_Public.thy
--- a/src/HOL/Auth/Guard/Guard_Public.thy	Sun Jul 15 22:56:49 2012 +0200
+++ b/src/HOL/Auth/Guard/Guard_Public.thy	Sun Jul 15 22:58:52 2012 +0200
@@ -5,7 +5,7 @@
 Lemmas on guarded messages for public protocols.
 *)
 
-theory Guard_Public imports Guard Public Extensions begin
+theory Guard_Public imports Guard "../Public" Extensions begin
 
 subsection{*Extensions to Theory @{text Public}*}
 
diff -r 429fab105d99 -r fa7e99b80675 src/HOL/Bali/AxExample.thy
--- a/src/HOL/Bali/AxExample.thy	Sun Jul 15 22:56:49 2012 +0200
+++ b/src/HOL/Bali/AxExample.thy	Sun Jul 15 22:58:52 2012 +0200
@@ -83,7 +83,7 @@
 apply   (tactic "ax_tac 1" (* AVar *))
 prefer 2
 apply    (rule ax_subst_Val_allI)
-apply    (tactic {* inst1_tac @{context} "P'" "\<lambda>u a. Normal (?PP a\<leftarrow>?x) u" *})
+apply    (tactic {* inst1_tac @{context} "P'" "\<lambda>a. Normal (?PP a\<leftarrow>?x)" *})
 apply    (simp del: avar_def2 peek_and_def2)
 apply    (tactic "ax_tac 1")
 apply   (tactic "ax_tac 1")
@@ -137,7 +137,7 @@
 prefer 4
 apply    (rule ax_derivs.Done [THEN conseq1],force)
 apply   (rule ax_subst_Val_allI)
-apply   (tactic {* inst1_tac @{context} "P'" "\<lambda>u a. Normal (?PP a\<leftarrow>?x) u" *})
+apply   (tactic {* inst1_tac @{context} "P'" "\<lambda>a. Normal (?PP a\<leftarrow>?x)" *})
 apply   (simp (no_asm) del: peek_and_def2 heap_free_def2 normal_def2 o_apply)
 apply   (tactic "ax_tac 1")
 prefer 2
@@ -161,7 +161,7 @@
 apply (tactic "ax_tac 1")
 defer
 apply  (rule ax_subst_Var_allI)
-apply  (tactic {* inst1_tac @{context} "P'" "\<lambda>u vf. Normal (?PP vf \<and>. ?p) u" *})
+apply  (tactic {* inst1_tac @{context} "P'" "\<lambda>vf. Normal (?PP vf \<and>. ?p)" *})
 apply  (simp (no_asm) del: split_paired_All peek_and_def2 initd_def2 heap_free_def2 normal_def2)
 apply  (tactic "ax_tac 1" (* NewC *))
 apply  (tactic "ax_tac 1" (* ax_Alloc *))
diff -r 429fab105d99 -r fa7e99b80675 src/Pure/search.ML
--- a/src/Pure/search.ML	Sun Jul 15 22:56:49 2012 +0200
+++ b/src/Pure/search.ML	Sun Jul 15 22:58:52 2012 +0200
@@ -255,9 +255,9 @@
 *)
 
 (*Insertion into priority queue of states, marked with level *)
-fun insert_with_level (lnth: int*int*thm, []) = [lnth]
-  | insert_with_level ((l,m,th), (l',n,th')::nths) =
-      if  n<m then (l',n,th') :: insert_with_level ((l,m,th), nths)
+fun insert_with_level (lnth: int*int*thm) [] = [lnth]
+  | insert_with_level (l,m,th) ((l',n,th') :: nths) =
+      if  n<m then (l',n,th') :: insert_with_level (l,m,th) nths
       else if  n=m andalso Thm.eq_thm(th,th')
               then (l',n,th')::nths
               else (l,m,th)::(l',n,th')::nths;
@@ -274,7 +274,7 @@
       let fun cost thm = (level, costf level thm, thm)
       in (case  List.partition satp news  of
             ([],nonsats)
-                 => next (List.foldr insert_with_level nprfs (map cost nonsats))
+                 => next (fold_rev (insert_with_level o cost) nonsats nprfs)
           | (sats,_)  => some_of_list sats)
       end and
       next []  = NONE
diff -r 429fab105d99 -r fa7e99b80675 src/Pure/term.ML
--- a/src/Pure/term.ML	Sun Jul 15 22:56:49 2012 +0200
+++ b/src/Pure/term.ML	Sun Jul 15 22:58:52 2012 +0200
@@ -147,7 +147,7 @@
   val aconv_untyped: term * term -> bool
   val could_unify: term * term -> bool
   val strip_abs_eta: int -> term -> (string * typ) list * term
-  val match_bvars: (term * term) * (string * string) list -> (string * string) list
+  val match_bvars: (term * term) -> (string * string) list -> (string * string) list
   val map_abs_vars: (string -> string) -> term -> term
   val rename_abs: term -> term -> term -> term option
   val is_open: term -> bool
@@ -611,7 +611,7 @@
   | match_bvs(_,_,al) = al;
 
 (* strip abstractions created by parameters *)
-fun match_bvars((s,t),al) = match_bvs(strip_abs_body s, strip_abs_body t, al);
+fun match_bvars (s,t) al = match_bvs(strip_abs_body s, strip_abs_body t, al);
 
 fun map_abs_vars f (t $ u) = map_abs_vars f t $ map_abs_vars f u
   | map_abs_vars f (Abs (a, T, t)) = Abs (f a, T, map_abs_vars f t)
diff -r 429fab105d99 -r fa7e99b80675 src/Pure/thm.ML
--- a/src/Pure/thm.ML	Sun Jul 15 22:56:49 2012 +0200
+++ b/src/Pure/thm.ML	Sun Jul 15 22:58:52 2012 +0200
@@ -1562,7 +1562,7 @@
 
 (*Function to rename bounds/unknowns in the argument, lifted over B*)
 fun rename_bvars dpairs =
-  rename_bvs (List.foldr Term.match_bvars [] dpairs) dpairs;
+  rename_bvs (fold_rev Term.match_bvars dpairs []) dpairs;
 
 
 (*** RESOLUTION ***)
diff -r 429fab105d99 -r fa7e99b80675 src/Pure/unify.ML
--- a/src/Pure/unify.ML	Sun Jul 15 22:56:49 2012 +0200
+++ b/src/Pure/unify.ML	Sun Jul 15 22:58:52 2012 +0200
@@ -273,11 +273,11 @@
   Does not even identify Vars in dpairs such as ?a =?= ?b; an attempt to
     do so caused numerous problems with no compensating advantage.
 *)
-fun SIMPL0 thy (dp0, (env,flexflex,flexrigid)) : Envir.env * dpair list * dpair list =
+fun SIMPL0 thy dp0 (env,flexflex,flexrigid) : Envir.env * dpair list * dpair list =
   let
     val (dp as (rbinder, t, u), env) = head_norm_dpair thy (env, dp0);
     fun SIMRANDS (f $ t, g $ u, env) =
-          SIMPL0 thy ((rbinder, t, u), SIMRANDS (f, g, env))
+          SIMPL0 thy (rbinder, t, u) (SIMRANDS (f, g, env))
       | SIMRANDS (t as _$_, _, _) =
           raise TERM ("SIMPL: operands mismatch", [t, u])
       | SIMRANDS (t, u as _ $ _, _) =
@@ -318,7 +318,7 @@
   Clever would be to re-do just the affected dpairs*)
 fun SIMPL thy (env,dpairs) : Envir.env * dpair list * dpair list =
   let
-    val all as (env', flexflex, flexrigid) = List.foldr (SIMPL0 thy) (env, [], []) dpairs;
+    val all as (env', flexflex, flexrigid) = fold_rev (SIMPL0 thy) dpairs (env, [], []);
     val dps = flexrigid @ flexflex;
   in
     if exists (fn (_, t, u) => changed (env', t) orelse changed (env', u)) dps
@@ -496,15 +496,24 @@
   in change 0 end;
 
 (*Change indices, delete the argument if it contains a banned Bound*)
-fun change_arg banned ({j, t, T}, args) : flarg list =
+fun change_arg banned {j, t, T} args : flarg list =
   if rigid_bound (0, banned) t then args  (*delete argument!*)
   else {j = j, t = change_bnos banned t, T = T} :: args;
 
 
 (*Sort the arguments to create assignments if possible:
-  create eta-terms like ?g(B.1,B.0) *)
-fun arg_less ({t = Bound i1, ...}, {t = Bound i2, ...}) = (i2 < i1)
-  | arg_less (_: flarg, _: flarg) = false;
+  create eta-terms like ?g B.1 B.0*)
+local
+  fun less_arg ({t = Bound i1, ...}, {t = Bound i2, ...}) = (i2 < i1)
+    | less_arg (_: flarg, _: flarg) = false;
+
+  fun ins_arg x [] = [x]
+    | ins_arg x (y :: ys) =
+        if less_arg (y, x) then y :: ins_arg x ys else x :: y :: ys;
+in
+  fun sort_args [] = []
+    | sort_args (x :: xs) = ins_arg x (sort_args xs);
+end;
 
 (*Test whether the new term would be eta-equivalent to a variable --
   if so then there is no point in creating a new variable*)
@@ -519,7 +528,7 @@
     val (Var (v, T), ts) = strip_comb t;
     val (Ts, U) = strip_type env T
     and js = length ts - 1  downto 0;
-    val args = sort (make_ord arg_less) (List.foldr (change_arg banned) [] (flexargs (js, ts, Ts)))
+    val args = sort_args (fold_rev (change_arg banned) (flexargs (js, ts, Ts)) [])
     val ts' = map #t args;
   in
     if decreasing (length Ts) args then (env, (list_comb (Var (v, T), ts')))
@@ -570,7 +579,7 @@
   eliminates trivial tpairs like t=t, as well as repeated ones
   trivial tpairs can easily escape SIMPL:  ?A=t, ?A=?B, ?B=t gives t=t
   Resulting tpairs MAY NOT be in normal form:  assignments may occur here.*)
-fun add_ffpair thy ((rbinder,t0,u0), (env,tpairs)) : Envir.env * (term * term) list =
+fun add_ffpair thy (rbinder,t0,u0) (env,tpairs) : Envir.env * (term * term) list =
   let
     val t = Envir.norm_term env t0
     and u = Envir.norm_term env u0;
@@ -618,7 +627,7 @@
             SIMPL thy (env, dpairs));
         in
           (case flexrigid of
-            [] => SOME (List.foldr (add_ffpair thy) (env', []) flexflex, reseq)
+            [] => SOME (fold_rev (add_ffpair thy) flexflex (env', []), reseq)
           | dp :: frigid' =>
               if tdepth > search_bnd then
                 (warning "Unification bound exceeded"; Seq.pull reseq)
@@ -655,7 +664,7 @@
   Unlike Huet (1975), does not smash together all variables of same type --
     requires more work yet gives a less general unifier (fewer variables).
   Handles ?f(t1...rm) with ?f(u1...um) to avoid multiple updates. *)
-fun smash_flexflex1 ((t, u), env) : Envir.env =
+fun smash_flexflex1 (t, u) env : Envir.env =
   let
     val vT as (v, T) = var_head_of (env, t)
     and wU as (w, U) = var_head_of (env, u);
@@ -669,7 +678,7 @@
 
 (*Smash all flex-flexpairs.  Should allow selection of pairs by a predicate?*)
 fun smash_flexflex (env, tpairs) : Envir.env =
-  List.foldr smash_flexflex1 env tpairs;
+  fold_rev smash_flexflex1 tpairs env;
 
 (*Returns unifiers with no remaining disagreement pairs*)
 fun smash_unifiers thy tus env =