1.1 --- a/src/Pure/Tools/find_theorems.ML	Thu Jul 18 21:57:27 2013 +0200
     1.2 +++ b/src/Pure/Tools/find_theorems.ML	Thu Jul 18 22:00:35 2013 +0200
     1.3 @@ -631,8 +631,18 @@
     1.4          Toplevel.keep (fn state =>
     1.5            let
     1.6              val ctxt = Toplevel.context_of state;
     1.7 +            val thy' =
     1.8 +              Proof_Context.theory_of ctxt
     1.9 +              |> Theory.copy
    1.10 +              |> Context_Position.set_visible_global (Context_Position.is_visible ctxt)
    1.11 +              |> Theory.checkpoint;
    1.12 +
    1.13              val opt_goal = try (Proof.simple_goal o Toplevel.proof_of) state |> Option.map #goal;
    1.14 -          in print_theorems ctxt opt_goal opt_lim rem_dups spec end)));
    1.15 +            val (ctxt', opt_goal') =
    1.16 +              (case opt_goal of
    1.17 +                NONE => (ctxt, NONE)
    1.18 +              | SOME th => (Proof_Context.transfer thy' ctxt, SOME (Thm.transfer thy' th)));
    1.19 +          in print_theorems ctxt' opt_goal' opt_lim rem_dups spec end)));
    1.20  
    1.21  end;
    1.22  

     2.1 --- a/src/Pure/unify.ML	Thu Jul 18 21:57:27 2013 +0200
     2.2 +++ b/src/Pure/unify.ML	Thu Jul 18 22:00:35 2013 +0200
     2.3 @@ -189,7 +189,10 @@
     2.4  fun test_unify_types thy (T, U) env =
     2.5    let
     2.6      val str_of = Syntax.string_of_typ_global thy;
     2.7 -    fun warn () = tracing ("Potential loss of completeness: " ^ str_of U ^ " = " ^ str_of T);
     2.8 +    fun warn () =
     2.9 +      if Context_Position.is_visible_global thy then
    2.10 +        tracing ("Potential loss of completeness: " ^ str_of U ^ " = " ^ str_of T)
    2.11 +      else ();
    2.12      val env' = unify_types thy (T, U) env;
    2.13    in if is_TVar T orelse is_TVar U then warn () else (); env' end;
    2.14  
    2.15 @@ -572,14 +575,16 @@
    2.16    In t==u print u first because it may be rigid or flexible --
    2.17      t is always flexible.*)
    2.18  fun print_dpairs thy msg (env, dpairs) =
    2.19 -  let
    2.20 -    fun pdp (rbinder, t, u) =
    2.21 -      let
    2.22 -        fun termT t =
    2.23 -          Syntax.pretty_term_global thy (Envir.norm_term env (Logic.rlist_abs (rbinder, t)));
    2.24 -        val bsymbs = [termT u, Pretty.str " =?=", Pretty.brk 1, termT t];
    2.25 -      in tracing (Pretty.string_of (Pretty.blk (0, bsymbs))) end;
    2.26 -  in tracing msg; List.app pdp dpairs end;
    2.27 +  if Context_Position.is_visible_global thy then
    2.28 +    let
    2.29 +      fun pdp (rbinder, t, u) =
    2.30 +        let
    2.31 +          fun termT t =
    2.32 +            Syntax.pretty_term_global thy (Envir.norm_term env (Logic.rlist_abs (rbinder, t)));
    2.33 +          val bsymbs = [termT u, Pretty.str " =?=", Pretty.brk 1, termT t];
    2.34 +        in tracing (Pretty.string_of (Pretty.blk (0, bsymbs))) end;
    2.35 +    in tracing msg; List.app pdp dpairs end
    2.36 +  else ();
    2.37  
    2.38  
    2.39  (*Unify the dpairs in the environment.
    2.40 @@ -602,7 +607,8 @@
    2.41              [] => SOME (fold_rev (add_ffpair thy) flexflex (env', []), reseq)
    2.42            | dp :: frigid' =>
    2.43                if tdepth > search_bound then
    2.44 -                (warning "Unification bound exceeded"; Seq.pull reseq)
    2.45 +                (Context_Position.if_visible_global thy warning "Unification bound exceeded";
    2.46 +                 Seq.pull reseq)
    2.47                else
    2.48                 (if tdepth > trace_bound then
    2.49                    print_dpairs thy "Enter MATCH" (env',flexrigid@flexflex)
    2.50 @@ -611,8 +617,8 @@
    2.51                      (add_unify (tdepth + 1)) (MATCH thy (env',dp, frigid'@flexflex), reseq))))
    2.52          end
    2.53          handle CANTUNIFY =>
    2.54 -         (if tdepth > trace_bound then tracing "Failure node" else ();
    2.55 -          Seq.pull reseq));
    2.56 +         (if tdepth > trace_bound then Context_Position.if_visible_global thy tracing "Failure node"
    2.57 +          else (); Seq.pull reseq));
    2.58      val dps = map (fn (t, u) => ([], t, u)) tus;
    2.59    in add_unify 1 ((env, dps), Seq.empty) end;
    2.60  

     3.1 --- a/src/Tools/solve_direct.ML	Thu Jul 18 21:57:27 2013 +0200
     3.2 +++ b/src/Tools/solve_direct.ML	Thu Jul 18 22:00:35 2013 +0200
     3.3 @@ -29,6 +29,7 @@
     3.4  val noneN = "none";
     3.5  val unknownN = "none";
     3.6  
     3.7 +
     3.8  (* preferences *)
     3.9  
    3.10  val max_solutions = Unsynchronized.ref 5;
    3.11 @@ -46,10 +47,11 @@
    3.12  fun do_solve_direct mode state =
    3.13    let
    3.14      val ctxt = Proof.context_of state;
    3.15 +    val find_ctxt = if mode = Auto_Try then Context_Position.set_visible false ctxt else ctxt;
    3.16  
    3.17      val crits = [(true, Find_Theorems.Solves)];
    3.18      fun find g =
    3.19 -      snd (Find_Theorems.find_theorems ctxt (SOME g) (SOME (! max_solutions)) false crits);
    3.20 +      snd (Find_Theorems.find_theorems find_ctxt (SOME g) (SOME (! max_solutions)) false crits);
    3.21  
    3.22      fun prt_result (goal, results) =
    3.23        let