# HG changeset patch
# User haftmann
# Date 1271683918 -7200
# Node ID 03a41196a9a0ffc0a7432111f5aa2ea403eb7565
# Parent  566be5d48090fdd3b1713bfdaf83770137925720
more appropriate representation of valid positions for abstractors

diff -r 566be5d48090 -r 03a41196a9a0 src/Tools/Code/code_thingol.ML
--- a/src/Tools/Code/code_thingol.ML	Mon Apr 19 15:31:56 2010 +0200
+++ b/src/Tools/Code/code_thingol.ML	Mon Apr 19 15:31:58 2010 +0200
@@ -655,10 +655,10 @@
             translate_app thy algbr eqngr some_abs some_thm ((c, ty), ts)
         | (t', ts) =>
             translate_term thy algbr eqngr some_abs some_thm t'
-            ##>> fold_map (translate_term thy algbr eqngr some_abs some_thm) ts
+            ##>> fold_map (translate_term thy algbr eqngr NONE some_thm) ts
             #>> (fn (t, ts) => t `$$ ts)
-and translate_eqn thy algbr eqngr ((some_abs, (args, rhs)), (some_thm, proper)) =
-  fold_map (translate_term thy algbr eqngr some_abs some_thm) args
+and translate_eqn thy algbr eqngr ((args, (rhs, some_abs)), (some_thm, proper)) =
+  fold_map (fn (arg, some_abs) => translate_term thy algbr eqngr some_abs some_thm arg) args
   ##>> translate_term thy algbr eqngr some_abs some_thm rhs
   #>> rpair (some_thm, proper)
 and translate_const thy algbr eqngr some_abs some_thm (c, ty) =
@@ -680,7 +680,7 @@
   end
 and translate_app_const thy algbr eqngr some_abs some_thm (c_ty, ts) =
   translate_const thy algbr eqngr some_abs some_thm c_ty
-  ##>> fold_map (translate_term thy algbr eqngr some_abs some_thm) ts
+  ##>> fold_map (translate_term thy algbr eqngr NONE some_thm) ts
   #>> (fn (t, ts) => t `$$ ts)
 and translate_case thy algbr eqngr some_abs some_thm (num_args, (t_pos, case_pats)) (c_ty, ts) =
   let
@@ -753,7 +753,7 @@
     translate_case thy algbr eqngr some_abs some_thm case_scheme ((c, ty), ts)
 and translate_app thy algbr eqngr some_abs some_thm (c_ty_ts as ((c, _), _)) =
   case Code.get_case_scheme thy c
-   of SOME case_scheme => translate_app_case thy algbr eqngr some_abs some_thm case_scheme c_ty_ts
+   of SOME case_scheme => translate_app_case thy algbr eqngr NONE some_thm case_scheme c_ty_ts
     | NONE => translate_app_const thy algbr eqngr some_abs some_thm c_ty_ts
 and translate_tyvar_sort thy (algbr as (proj_sort, _)) eqngr (v, sort) =
   fold_map (ensure_class thy algbr eqngr) (proj_sort sort)