src/HOL/Tools/Nitpick/nitpick_model.ML
changeset 38207 792b78e355e7
parent 38190 b02e204b613a
child 38209 3d1d928dce50
     1.1 --- a/src/HOL/Tools/Nitpick/nitpick_model.ML	Thu Aug 05 15:44:54 2010 +0200
     1.2 +++ b/src/HOL/Tools/Nitpick/nitpick_model.ML	Thu Aug 05 18:00:50 2010 +0200
     1.3 @@ -779,7 +779,7 @@
     1.4           (Const (step_name, T --> T) $ Const (unprefix step_prefix s, T),
     1.5            format_type default_format default_format T)
     1.6         else if String.isPrefix quot_normal_prefix s then
     1.7 -         let val t = Const (nitpick_prefix ^ "normalize quotient type", T) in
     1.8 +         let val t = Const (nitpick_prefix ^ "quotient normal form", T) in
     1.9             (t, format_term_type thy def_table formats t)
    1.10           end
    1.11         else if String.isPrefix skolem_prefix s then