# HG changeset patch
# User wenzelm
# Date 1374175209 -7200
# Node ID abed4121c17e55b912bc113717cbd185eabf6f22
# Parent  df1531af559f2b9f2b8afd703d569f3f6c7629b3
tuned signature;

diff -r df1531af559f -r abed4121c17e src/HOL/Tools/SMT/smt_config.ML
--- a/src/HOL/Tools/SMT/smt_config.ML	Thu Jul 18 21:06:21 2013 +0200
+++ b/src/HOL/Tools/SMT/smt_config.ML	Thu Jul 18 21:20:09 2013 +0200
@@ -101,9 +101,10 @@
 fun available_solvers_of ctxt =
   filter (is_available ctxt) (all_solvers_of ctxt)
 
-fun warn_solver context name =
-  Context_Position.if_visible_proof context
-    warning ("The SMT solver " ^ quote name ^ " is not installed.")
+fun warn_solver (Context.Proof ctxt) name =
+      Context_Position.if_visible ctxt
+        warning ("The SMT solver " ^ quote name ^ " is not installed.")
+  | warn_solver _ _ = ();
 
 fun select_solver name context =
   let
diff -r df1531af559f -r abed4121c17e src/Provers/classical.ML
--- a/src/Provers/classical.ML	Thu Jul 18 21:06:21 2013 +0200
+++ b/src/Provers/classical.ML	Thu Jul 18 21:20:09 2013 +0200
@@ -302,10 +302,10 @@
     error ("Ill-formed destruction rule\n" ^ string_of_thm context th)
   else Tactic.make_elim th;
 
-fun warn_thm opt_context msg th =
-  if (case opt_context of SOME context => Context_Position.is_visible_proof context | NONE => false)
-  then warning (msg ^ string_of_thm opt_context th)
-  else ();
+fun warn_thm (SOME (Context.Proof ctxt)) msg th =
+      if Context_Position.is_visible ctxt
+      then warning (msg ^ Display.string_of_thm ctxt th) else ()
+  | warn_thm _ _ _ = ();
 
 fun warn_rules context msg rules th =
   Item_Net.member rules th andalso (warn_thm context msg th; true);
diff -r df1531af559f -r abed4121c17e src/Pure/context_position.ML
--- a/src/Pure/context_position.ML	Thu Jul 18 21:06:21 2013 +0200
+++ b/src/Pure/context_position.ML	Thu Jul 18 21:20:09 2013 +0200
@@ -10,8 +10,6 @@
   val set_visible: bool -> Proof.context -> Proof.context
   val restore_visible: Proof.context -> Proof.context -> Proof.context
   val if_visible: Proof.context -> ('a -> unit) -> 'a -> unit
-  val is_visible_proof: Context.generic -> bool
-  val if_visible_proof: Context.generic -> ('a -> unit) -> 'a -> unit
   val report_generic: Context.generic -> Position.T -> Markup.T -> unit
   val reported_text: Proof.context -> Position.T -> Markup.T -> string -> string
   val report_text: Proof.context -> Position.T -> Markup.T -> string -> unit
@@ -38,11 +36,6 @@
 
 fun if_visible ctxt f x = if is_visible ctxt then f x else ();
 
-fun is_visible_proof (Context.Proof ctxt) = is_visible ctxt
-  | is_visible_proof _ = false;
-
-fun if_visible_proof context f x = if is_visible_proof context then f x else ();
-
 fun report_generic context pos markup =
   if is_visible_generic context then
     Output.report (Position.reported_text pos markup "")