src/HOL/Tools/BNF/bnf_fp_n2m.ML
changeset 57527 1b07ca054327
parent 57397 5004aca20821
child 57700 a2c4adb839a9
     1.1 --- a/src/HOL/Tools/BNF/bnf_fp_n2m.ML	Mon Jul 07 16:06:46 2014 +0200
     1.2 +++ b/src/HOL/Tools/BNF/bnf_fp_n2m.ML	Mon Jul 07 16:06:46 2014 +0200
     1.3 @@ -299,7 +299,7 @@
     1.4          val i = find_index (fn T => x = T) Xs;
     1.5          val TUrec =
     1.6            (case find_first (fn f => body_fun_type (fastype_of f) = TU) recs of
     1.7 -            NONE => 
     1.8 +            NONE =>
     1.9                force_rec i TU
    1.10                  (TU |> is_none b_opt ? substT (map2 mk_co_productT fpTs Xs ~~ Xs)) (nth co_recs i)
    1.11            | SOME f => f);
    1.12 @@ -368,7 +368,7 @@
    1.13        fold2 (fn TU => fn b => fn ((recs, defs), lthy) =>
    1.14          mk_rec (SOME b) recs lthy TU |>> (fn (f, d) => (f :: recs, d :: defs)))
    1.15        resTs (map (Binding.suffix_name ("_" ^ recN)) bs) (([], []), lthy)
    1.16 -      |>> apfst rev o apsnd rev;
    1.17 +      |>> map_prod rev rev;
    1.18      val ((raw_co_recs, raw_co_rec_defs), (lthy, raw_lthy)) = lthy
    1.19        |> mk_recs
    1.20        ||> `Local_Theory.restore;