tuned;
authorwenzelm
Sun Dec 03 19:00:55 2017 +0100 (6 weeks ago)
changeset 67121116968454d70
parent 67120 491fd7f0b5df
child 67122 85b40f300fab
tuned;
src/HOL/Word/WordBitwise.thy
     1.1 --- a/src/HOL/Word/WordBitwise.thy	Sun Dec 03 18:53:49 2017 +0100
     1.2 +++ b/src/HOL/Word/WordBitwise.thy	Sun Dec 03 19:00:55 2017 +0100
     1.3 @@ -416,9 +416,8 @@
     1.4  val word_ss = simpset_of @{theory_context Word};
     1.5  
     1.6  fun mk_nat_clist ns =
     1.7 -  List.foldr
     1.8 -    (uncurry (Thm.mk_binop @{cterm "Cons :: nat \<Rightarrow> _"}))
     1.9 -    @{cterm "[] :: nat list"} ns;
    1.10 +  fold_rev (Thm.mk_binop @{cterm "Cons :: nat \<Rightarrow> _"})
    1.11 +    ns @{cterm "[] :: nat list"};
    1.12  
    1.13  fun upt_conv ctxt ct =
    1.14    case Thm.term_of ct of
    1.15 @@ -471,8 +470,7 @@
    1.16        (case arg of @{term nat} $ n => n | n => n)
    1.17        |> HOLogic.dest_number |> snd;
    1.18      val (i, j) = if n > n_sucs then (n_sucs, n - n_sucs) else (n, 0);
    1.19 -    val arg' =
    1.20 -      List.foldr (op $) (HOLogic.mk_number @{typ nat} j) (replicate i @{term Suc});
    1.21 +    val arg' = funpow i HOLogic.mk_Suc (HOLogic.mk_number @{typ nat} j);
    1.22      val _ = if arg = arg' then raise TERM ("", []) else ();
    1.23      fun propfn g =
    1.24        HOLogic.mk_eq (g arg, g arg')