# HG changeset patch
# User wenzelm
# Date 1237988828 -3600
# Node ID e23e15f52d4232e277f17c889404c81558c45df4
# Parent  88bc86d7dec3814562530f5b176cad0067806a02
avoid mixing of left/right associative infixes, to make it work with experimental Poly/ML 5.3 branch;

diff -r 88bc86d7dec3 -r e23e15f52d42 src/HOL/SizeChange/sct.ML
--- a/src/HOL/SizeChange/sct.ML	Tue Mar 24 23:43:58 2009 +0100
+++ b/src/HOL/SizeChange/sct.ML	Wed Mar 25 14:47:08 2009 +0100
@@ -105,7 +105,7 @@
 
 fun dest_case rebind t =
     let
-      val (_ $ _ $ rhs :: _ $ _ $ match :: guards) = HOLogic.dest_conj t
+      val ((_ $ _ $ rhs) :: (_ $ _ $ match) :: guards) = HOLogic.dest_conj t
       val guard = case guards of [] => HOLogic.true_const | gs => foldr1 HOLogic.mk_conj gs
     in
       foldr1 HOLogic.mk_prod [rebind guard, rebind rhs, rebind match]
diff -r 88bc86d7dec3 -r e23e15f52d42 src/HOL/Tools/function_package/lexicographic_order.ML
--- a/src/HOL/Tools/function_package/lexicographic_order.ML	Tue Mar 24 23:43:58 2009 +0100
+++ b/src/HOL/Tools/function_package/lexicographic_order.ML	Wed Mar 25 14:47:08 2009 +0100
@@ -176,7 +176,7 @@
 
       val gc = map (fn i => chr (i + 96)) (1 upto length table)
       val mc = 1 upto length measure_funs
-      val tstr = "Result matrix:" ::  "   " ^ concat (map (enclose " " " " o string_of_int) mc)
+      val tstr = "Result matrix:" ::  ("   " ^ concat (map (enclose " " " " o string_of_int) mc))
                  :: map2 (fn r => fn i => i ^ ": " ^ concat (map pr_cell r)) table gc
       val gstr = "Calls:" :: map2 (prefix "  " oo pr_goal) tl gc
       val mstr = "Measures:" :: map2 (prefix "  " oo pr_fun) measure_funs mc
diff -r 88bc86d7dec3 -r e23e15f52d42 src/HOL/Tools/record_package.ML
--- a/src/HOL/Tools/record_package.ML	Tue Mar 24 23:43:58 2009 +0100
+++ b/src/HOL/Tools/record_package.ML	Wed Mar 25 14:47:08 2009 +0100
@@ -1782,7 +1782,8 @@
     val alphas_fields = List.foldr OldTerm.add_typ_tfree_names [] types;
     val alphas_ext = alphas inter alphas_fields;
     val len = length fields;
-    val variants = Name.variant_list (moreN::rN::rN ^ "'"::wN::parent_variants) (map fst bfields);
+    val variants =
+      Name.variant_list (moreN :: rN :: (rN ^ "'") :: wN :: parent_variants) (map fst bfields);
     val vars = ListPair.map Free (variants, types);
     val named_vars = names ~~ vars;
     val idxs = 0 upto (len - 1);