src/HOL/Tools/Ctr_Sugar/local_interpretation.ML
changeset 58182 82478e6c60cb
parent 58178 695ba3101b37
child 58185 e6e3b20340be
     1.1 --- a/src/HOL/Tools/Ctr_Sugar/local_interpretation.ML	Thu Sep 04 09:02:43 2014 +0200
     1.2 +++ b/src/HOL/Tools/Ctr_Sugar/local_interpretation.ML	Thu Sep 04 11:20:59 2014 +0200
     1.3 @@ -42,11 +42,13 @@
     1.4      val (data, interps) = Interp.get thy;
     1.5      val unfinished = interps |> map (fn ((gf, _), xs) =>
     1.6        (g_or_f gf, if eq_list eq (xs, data) then [] else subtract eq xs data));
     1.7 -    val finished = interps |> map (fn (interp, _) => (interp, data));
     1.8 +    val finished = interps |> map (apsnd (K data));
     1.9    in
    1.10 -    if forall (null o #2) unfinished then NONE
    1.11 -    else SOME (thy_or_lthy |> fold_rev (uncurry fold_rev) unfinished
    1.12 -      |> lift_lthy (Interp.put (data, finished)))
    1.13 +    if forall (null o #2) unfinished then
    1.14 +      NONE
    1.15 +    else
    1.16 +      SOME (thy_or_lthy |> fold_rev (uncurry fold_rev) unfinished
    1.17 +        |> lift_lthy (Interp.put (data, finished)))
    1.18    end;
    1.19  
    1.20  fun consolidate lthy =