src/HOL/Tools/Nitpick/nitpick_hol.ML
changeset 44241 7943b69f0188
parent 44017 e828be67dfe7
child 45272 5995ab88a00f
     1.1 --- a/src/HOL/Tools/Nitpick/nitpick_hol.ML	Wed Aug 17 16:46:58 2011 +0200
     1.2 +++ b/src/HOL/Tools/Nitpick/nitpick_hol.ML	Wed Aug 17 18:05:31 2011 +0200
     1.3 @@ -1555,7 +1555,7 @@
     1.4      else
     1.5        fst (hd cases) |> fold_rev (add_constr_case res_T) (tl cases)
     1.6    end
     1.7 -  |> curry absdummy dataT
     1.8 +  |> absdummy dataT
     1.9  
    1.10  fun optimized_record_get (hol_ctxt as {thy, ctxt, stds, ...}) s rec_T res_T t =
    1.11    let val constr_x = hd (datatype_constrs hol_ctxt rec_T) in
    1.12 @@ -1968,7 +1968,7 @@
    1.13            discriminate_value hol_ctxt x y_var ::
    1.14            map2 (nth_sub_bisim x) (index_seq 0 (length arg_Ts)) arg_Ts
    1.15            |> foldr1 s_conj
    1.16 -      in List.foldr absdummy core_t arg_Ts end
    1.17 +      in fold_rev absdummy arg_Ts core_t end
    1.18    in
    1.19      [HOLogic.mk_imp
    1.20         (HOLogic.mk_disj (HOLogic.eq_const iter_T $ n_var $ zero_const iter_T,