1.1 --- a/src/HOL/Tools/Nitpick/nitpick_model.ML	Thu Jan 14 17:06:35 2010 +0100
     1.2 +++ b/src/HOL/Tools/Nitpick/nitpick_model.ML	Wed Jan 20 10:38:06 2010 +0100
     1.3 @@ -440,7 +440,9 @@
     1.4                        | _ => raise TERM ("Nitpick_Model.reconstruct_term.term_\
     1.5                                           \for_atom (Abs_Frac)", ts)
     1.6                      end
     1.7 -                  else if not for_auto andalso is_abs_fun thy constr_x then
     1.8 +                  else if not for_auto andalso
     1.9 +                          (is_abs_fun thy constr_x orelse
    1.10 +                           constr_s = @{const_name Quot}) then
    1.11                      Const (abs_name, constr_T) $ the_single ts
    1.12                    else
    1.13                      list_comb (Const constr_x, ts)
    1.14 @@ -560,8 +562,8 @@
    1.15              pairself (strip_comb o unfold_outer_the_binders) (t1, t2)
    1.16            val max_depth = max_depth - (if member (op =) coTs T then 1 else 0)
    1.17          in
    1.18 -          head1 = head2
    1.19 -          andalso forall (bisimilar_values coTs max_depth) (args1 ~~ args2)
    1.20 +          head1 = head2 andalso
    1.21 +          forall (bisimilar_values coTs max_depth) (args1 ~~ args2)
    1.22          end
    1.23        else
    1.24          t1 = t2
    1.25 @@ -704,8 +706,8 @@
    1.26    in
    1.27      (Pretty.chunks (if null chunks then [Pretty.str "Empty assignment"]
    1.28                      else chunks),
    1.29 -     bisim_depth >= 0
    1.30 -     orelse forall (is_codatatype_wellformed codatatypes) codatatypes)
    1.31 +     bisim_depth >= 0 orelse
    1.32 +     forall (is_codatatype_wellformed codatatypes) codatatypes)
    1.33    end
    1.34  
    1.35  (* scope -> Time.time option -> nut list -> nut list -> nut NameTable.table