# HG changeset patch
# User wenzelm
# Date 1342366039 -7200
# Node ID a0d8abca8d7ab5f29db3213381b7a9527d7fb936
# Parent  865610355ef376e1b1d93aaebd6193dfcd1d2ad1
back to naive insertion sort before 1997 to accommodate peculiar less_arg relation -- NB: make_ord arg_less was not a quasi-order and thus inappropriate for generic sort (cf. de74b549f976, ecfeff48bf0c);

diff -r 865610355ef3 -r a0d8abca8d7a src/HOL/Bali/AxExample.thy
--- a/src/HOL/Bali/AxExample.thy	Sun Jul 15 16:53:50 2012 +0200
+++ b/src/HOL/Bali/AxExample.thy	Sun Jul 15 17:27:19 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 865610355ef3 -r a0d8abca8d7a src/Pure/unify.ML
--- a/src/Pure/unify.ML	Sun Jul 15 16:53:50 2012 +0200
+++ b/src/Pure/unify.ML	Sun Jul 15 17:27:19 2012 +0200
@@ -502,9 +502,18 @@
 
 
 (*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 (List.foldr (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')))