1.1 --- a/src/Tools/Code/code_thingol.ML	Mon Apr 19 15:31:56 2010 +0200
     1.2 +++ b/src/Tools/Code/code_thingol.ML	Mon Apr 19 15:31:58 2010 +0200
     1.3 @@ -655,10 +655,10 @@
     1.4              translate_app thy algbr eqngr some_abs some_thm ((c, ty), ts)
     1.5          | (t', ts) =>
     1.6              translate_term thy algbr eqngr some_abs some_thm t'
     1.7 -            ##>> fold_map (translate_term thy algbr eqngr some_abs some_thm) ts
     1.8 +            ##>> fold_map (translate_term thy algbr eqngr NONE some_thm) ts
     1.9              #>> (fn (t, ts) => t `$$ ts)
    1.10 -and translate_eqn thy algbr eqngr ((some_abs, (args, rhs)), (some_thm, proper)) =
    1.11 -  fold_map (translate_term thy algbr eqngr some_abs some_thm) args
    1.12 +and translate_eqn thy algbr eqngr ((args, (rhs, some_abs)), (some_thm, proper)) =
    1.13 +  fold_map (fn (arg, some_abs) => translate_term thy algbr eqngr some_abs some_thm arg) args
    1.14    ##>> translate_term thy algbr eqngr some_abs some_thm rhs
    1.15    #>> rpair (some_thm, proper)
    1.16  and translate_const thy algbr eqngr some_abs some_thm (c, ty) =
    1.17 @@ -680,7 +680,7 @@
    1.18    end
    1.19  and translate_app_const thy algbr eqngr some_abs some_thm (c_ty, ts) =
    1.20    translate_const thy algbr eqngr some_abs some_thm c_ty
    1.21 -  ##>> fold_map (translate_term thy algbr eqngr some_abs some_thm) ts
    1.22 +  ##>> fold_map (translate_term thy algbr eqngr NONE some_thm) ts
    1.23    #>> (fn (t, ts) => t `$$ ts)
    1.24  and translate_case thy algbr eqngr some_abs some_thm (num_args, (t_pos, case_pats)) (c_ty, ts) =
    1.25    let
    1.26 @@ -753,7 +753,7 @@
    1.27      translate_case thy algbr eqngr some_abs some_thm case_scheme ((c, ty), ts)
    1.28  and translate_app thy algbr eqngr some_abs some_thm (c_ty_ts as ((c, _), _)) =
    1.29    case Code.get_case_scheme thy c
    1.30 -   of SOME case_scheme => translate_app_case thy algbr eqngr some_abs some_thm case_scheme c_ty_ts
    1.31 +   of SOME case_scheme => translate_app_case thy algbr eqngr NONE some_thm case_scheme c_ty_ts
    1.32      | NONE => translate_app_const thy algbr eqngr some_abs some_thm c_ty_ts
    1.33  and translate_tyvar_sort thy (algbr as (proj_sort, _)) eqngr (v, sort) =
    1.34    fold_map (ensure_class thy algbr eqngr) (proj_sort sort)