Swapped order of params.

--- a/src/HOL/Lex/AutoChopper.ML	Wed May 20 18:58:13 1998 +0200
+++ b/src/HOL/Lex/AutoChopper.ML	Mon May 25 12:55:01 1998 +0200
@@ -34,7 +34,7 @@
 qed"acc_prefix_Cons";
 Addsimps [acc_prefix_Cons];
 
-goal thy "!st us p y ys. acc A st p xs (ys@[y]) us ~= ([],zs)";
+goal thy "!st us p y ys. acc A st p (ys@[y]) xs us ~= ([],zs)";
 by (induct_tac "xs" 1);
 by (Simp_tac 1);
 by (Asm_simp_tac 1);
@@ -42,7 +42,7 @@
 Addsimps [accept_not_Nil];
 
 goal thy
-"!st us. acc A st ([],ys) xs [] us = ([], zs) --> \
+"!st us. acc A st ([],ys) [] xs us = ([], zs) --> \
 \        zs = ys & (!ys. ys ~= [] & ys<=xs --> ~fin A (delta A ys st))";
 by (induct_tac "xs" 1);
 by (simp_tac (simpset() addcongs [conj_cong]) 1);
@@ -69,12 +69,12 @@
 
 goal thy
 "! r erk l rst st ys yss zs::'a list. \
-\    acc A st (l,rst) xs erk r = (ys#yss, zs) --> \
+\    acc A st (l,rst) erk xs r = (ys#yss, zs) --> \
 \    ys@concat(yss)@zs = (if acc_prefix A xs st then r@xs else erk@concat(l)@rst)";
 by (induct_tac "xs" 1);
  by (simp_tac (simpset() addcongs [conj_cong]) 1);
 by (Asm_simp_tac 1);
-by (res_inst_tac [("p","acc A (start A) ([],list) list [] []")] PairE 1);
+by (res_inst_tac [("p","acc A (start A) ([],list) [] list []")] PairE 1);
 by (rename_tac "vss lrst" 1);  
 by (Asm_simp_tac 1);
 by (res_inst_tac[("xs","vss")] list_eq_cases 1);
@@ -88,7 +88,7 @@
 
 goal thy
  "! st erk r l rest ys yss zs.\
-\   acc A st (l,rest) xs erk r = (ys#yss, zs) --> \
+\   acc A st (l,rest) erk xs r = (ys#yss, zs) --> \
 \     (if acc_prefix A xs st \
 \      then ys ~= [] \
 \      else ys ~= [] | (erk=[] & (l,rest) = (ys#yss,zs)))";
@@ -97,7 +97,7 @@
  by (simp_tac (simpset() addcongs [conj_cong]) 1);
  by (Fast_tac 1);
 by (asm_simp_tac (simpset() addcongs [conj_cong]) 1);
-by (res_inst_tac [("p","acc A (start A) ([],list) list [] []")] PairE 1);
+by (res_inst_tac [("p","acc A (start A) ([],list) [] list []")] PairE 1);
 by (rename_tac "vss lrst" 1);  
 by (Asm_simp_tac 1);
 by (strip_tac 1);
@@ -111,7 +111,7 @@
 
 goal thy  
  "! st erk r l rest ys yss zs. \
-\   acc A st (l,rest) xs erk r = (ys#yss, zs) --> \
+\   acc A st (l,rest) erk xs r = (ys#yss, zs) --> \
 \     (if acc_prefix A xs st                   \
 \      then ? g. ys=r@g & fin A (delta A g st)  \
 \      else (erk~=[] & erk=ys) | (erk=[] & (l,rest) = (ys#yss,zs)))";
@@ -122,7 +122,7 @@
 by (asm_simp_tac (simpset() addcongs [conj_cong]) 1);
 by (strip_tac 1);
 by (rtac conjI 1);
- by (res_inst_tac [("p","acc A (start A) ([],list) list [] []")] PairE 1);
+ by (res_inst_tac [("p","acc A (start A) ([],list) [] list []")] PairE 1);
  by (rename_tac "vss lrst" 1);  
  by (Asm_simp_tac 1);
  by (case_tac "acc_prefix A list (next A a st)" 1);
@@ -150,22 +150,22 @@
 
 goal thy
  "! st erk r l rest ys yss zs. \
-\   acc A st (l,rest) xs erk r = (ys#yss, zs) --> \
+\   acc A st (l,rest) erk xs r = (ys#yss, zs) --> \
 \     (if acc_prefix A xs st       \
-\      then acc A (start A) ([],concat(yss)@zs) (concat(yss)@zs) [] [] = (yss,zs) \
+\      then acc A (start A) ([],concat(yss)@zs) [] (concat(yss)@zs) [] = (yss,zs) \
 \      else (erk~=[] & (l,rest)=(yss,zs)) | (erk=[] & (l, rest)=(ys#yss,zs)))";
 by (Simp_tac 1);
 by (induct_tac "xs" 1);
  by (simp_tac (simpset() addcongs [conj_cong]) 1);
  by (Fast_tac 1);
 by (asm_simp_tac (simpset() addcongs [conj_cong]) 1);
-by (res_inst_tac [("p","acc A (start A) ([],list) list [] []")] PairE 1);
+by (res_inst_tac [("p","acc A (start A) ([],list) [] list []")] PairE 1);
 by (rename_tac "vss lrst" 1);  
 by (Asm_simp_tac 1);
 by (strip_tac 1);
 by (case_tac "acc_prefix A list (next A a st)" 1);
  by (Asm_simp_tac 1);
-by (subgoal_tac "acc A (start A) ([],list) list [] [] = (yss,zs)" 1);
+by (subgoal_tac "acc A (start A) ([],list) [] list [] = (yss,zs)" 1);
  by (Asm_simp_tac 2);
  by (subgoal_tac "r@[a] ~= []" 2);
   by (Fast_tac 2);
@@ -189,7 +189,7 @@
 Delsimps [split_paired_All];
 goal thy 
 "! st erk r p ys yss zs. \
-\  acc A st p xs erk r = (ys#yss, zs) --> \
+\  acc A st p erk xs r = (ys#yss, zs) --> \
 \  (if acc_prefix A xs st  \
 \   then ? g. ys=r@g & (!as. as<=xs & g<=as & g~=as --> ~fin A (delta A as st))\
 \   else (erk~=[] & ys=erk) | (erk=[] & (ys#yss,zs)=p))";

--- a/src/HOL/Lex/AutoChopper.thy	Wed May 20 18:58:13 1998 +0200
+++ b/src/HOL/Lex/AutoChopper.thy	Mon May 25 12:55:01 1998 +0200
@@ -30,17 +30,17 @@
   acc :: "[('a,'s)da, 's, 'a list list*'a list, 'a list, 'a list, 'a list]
           => 'a list list * 'a list"
 primrec acc List.list
-  "acc A s r []     ys zs = (if ys=[] then r else (ys#fst(r),snd(r)))" 
-  "acc A s r (x#xs) ys zs =
+  "acc A s r ps []     zs = (if ps=[] then r else (ps#fst(r),snd(r)))" 
+  "acc A s r ps (x#xs) zs =
             (let t = next A x s
              in if fin A t
-                then acc A t (acc A (start A) ([],xs) xs [] [])
-                         xs (zs@[x]) (zs@[x])
-                else acc A t r xs ys (zs@[x]))"
+                then acc A t (acc A (start A) ([],xs) [] xs [])
+                         (zs@[x]) xs (zs@[x])
+                else acc A t r ps xs (zs@[x]))"
 
 constdefs
  auto_chopper :: ('a,'s)da => 'a chopper
-"auto_chopper A xs == acc A (start A) ([],xs) xs [] []"
+"auto_chopper A xs == acc A (start A) ([],xs) [] xs []"
 
 (* acc_prefix is an auxiliary notion for the proof *)
 constdefs