# HG changeset patch
# User wenzelm
# Date 1392926664 -3600
# Node ID 306ff289da3a2a5b402147cb02fffafb91396546
# Parent  460f4801b5cbd49bae6a6ca049ae7159f73d6367
tuned messages;
more official hyps;

diff -r 460f4801b5cb -r 306ff289da3a src/Tools/coherent.ML
--- a/src/Tools/coherent.ML	Thu Feb 20 20:59:15 2014 +0100
+++ b/src/Tools/coherent.ML	Thu Feb 20 21:04:24 2014 +0100
@@ -114,9 +114,8 @@
       end;
 
 fun string_of_facts ctxt s facts =
-  cat_lines
-    (s :: map (Syntax.string_of_term ctxt)
-      (map fst (sort (int_ord o pairself snd) (Net.content facts)))) ^ "\n\n";
+  Pretty.string_of (Pretty.big_list s
+    (map (Syntax.pretty_term ctxt) (map fst (sort (int_ord o pairself snd) (Net.content facts)))));
 
 fun valid ctxt rules goal dom facts nfacts nparams =
   let
@@ -133,7 +132,10 @@
           end));
   in
     (case Seq.pull seq of
-      NONE => (tracing (string_of_facts ctxt "Countermodel found:" facts); NONE)
+      NONE =>
+        (if Context_Position.is_visible ctxt then
+          warning (string_of_facts ctxt "Countermodel found:" facts)
+         else (); NONE)
     | SOME ((th, env, inst, is, cs), _) =>
         if cs = [([], [goal])] then SOME (ClPrf (th, env, inst, is, []))
         else
@@ -145,7 +147,11 @@
 and valid_cases _ _ _ _ _ _ _ [] = SOME []
   | valid_cases ctxt rules goal dom facts nfacts nparams ((Ts, ts) :: ds) =
       let
-        val _ = cond_trace ctxt (fn () => "case " ^ commas (map (Syntax.string_of_term ctxt) ts));
+        val _ =
+          cond_trace ctxt (fn () =>
+            Pretty.string_of (Pretty.block
+              (Pretty.str "case" :: Pretty.brk 1 ::
+                Pretty.commas (map (Syntax.pretty_term ctxt) ts))));
         val params = map_index (fn (i, T) => Free ("par" ^ string_of_int (nparams + i), T)) Ts;
         val ts' = map_index (fn (i, t) => (subst_bounds (rev params, t), nfacts + i)) ts;
         val dom' =
@@ -170,7 +176,7 @@
     val certT = Thm.ctyp_of thy;
     val _ =
       cond_trace ctxt (fn () =>
-        cat_lines ("asms:" :: map (Display.string_of_thm ctxt) asms) ^ "\n\n");
+        Pretty.string_of (Pretty.big_list "asms:" (map (Display.pretty_thm ctxt) asms)));
     val th' =
       Drule.implies_elim_list
         (Thm.instantiate
@@ -197,10 +203,10 @@
     val cert = Thm.cterm_of thy;
     val cparams = map cert params;
     val asms'' = map (cert o curry subst_bounds (rev params)) asms';
+    val (prems'', ctxt') = fold_map Thm.assume_hyps asms'' ctxt;
   in
     Drule.forall_intr_list cparams
-      (Drule.implies_intr_list asms''
-        (thm_of_cl_prf ctxt goal (asms @ map Thm.assume asms'') prf))
+      (Drule.implies_intr_list asms'' (thm_of_cl_prf ctxt' goal (asms @ prems'') prf))
   end;