src/HOL/Tools/refute.ML
changeset 39050 600de0485859
parent 39049 423b72f2d242
child 39809 dac3c3106746
     1.1 --- a/src/HOL/Tools/refute.ML	Fri Sep 03 10:58:11 2010 +0200
     1.2 +++ b/src/HOL/Tools/refute.ML	Fri Sep 03 11:21:58 2010 +0200
     1.3 @@ -268,8 +268,8 @@
     1.4          "Size of types: " ^ commas (map (fn (T, i) =>
     1.5            Syntax.string_of_typ ctxt T ^ ": " ^ string_of_int i) typs) ^ "\n"
     1.6      val show_consts_msg =
     1.7 -      if not (!show_consts) andalso Library.exists (is_Const o fst) terms then
     1.8 -        "set \"show_consts\" to show the interpretation of constants\n"
     1.9 +      if not (Config.get ctxt show_consts) andalso Library.exists (is_Const o fst) terms then
    1.10 +        "enable \"show_consts\" to show the interpretation of constants\n"
    1.11        else
    1.12          ""
    1.13      val terms_msg =
    1.14 @@ -278,7 +278,7 @@
    1.15        else
    1.16          cat_lines (map_filter (fn (t, intr) =>
    1.17            (* print constants only if 'show_consts' is true *)
    1.18 -          if (!show_consts) orelse not (is_Const t) then
    1.19 +          if Config.get ctxt show_consts orelse not (is_Const t) then
    1.20              SOME (Syntax.string_of_term ctxt t ^ ": " ^
    1.21                Syntax.string_of_term ctxt
    1.22                  (print ctxt model (Term.type_of t) intr assignment))