merged, resolving trivial conflict;
authorwenzelm
Wed Jul 22 11:23:09 2009 +0200 (2009-07-22)
changeset 321317913823f14e3
parent 32130 2a0645733185
parent 32110 eff525e07a31
child 32132 29aed5725acb
merged, resolving trivial conflict;
NEWS
src/HOL/Tools/inductive_realizer.ML
src/Pure/Isar/code.ML
src/Tools/Code/code_preproc.ML
src/Tools/Code/code_thingol.ML
     1.1 --- a/Admin/isatest/isatest-makedist	Wed Jul 22 10:49:26 2009 +0200
     1.2 +++ b/Admin/isatest/isatest-makedist	Wed Jul 22 11:23:09 2009 +0200
     1.3 @@ -110,8 +110,8 @@
     1.4  sleep 15
     1.5  $SSH macbroy5 "$MAKEALL $HOME/settings/mac-poly"
     1.6  sleep 15
     1.7 -$SSH macbroy6 "$MAKEALL $HOME/settings/at-mac-poly-5.1-para"
     1.8 -sleep 15
     1.9 +#$SSH macbroy6 "$MAKEALL $HOME/settings/at-mac-poly-5.1-para"
    1.10 +#sleep 15
    1.11  $SSH atbroy51 "$HOME/admin/isatest/isatest-annomaly"
    1.12  
    1.13  echo ------------------- spawned tests successfully --- `date` --- $HOSTNAME >> $DISTLOG 2>&1
     2.1 --- a/Admin/isatest/settings/mac-poly-M4	Wed Jul 22 10:49:26 2009 +0200
     2.2 +++ b/Admin/isatest/settings/mac-poly-M4	Wed Jul 22 11:23:09 2009 +0200
     2.3 @@ -4,7 +4,7 @@
     2.4    ML_SYSTEM="polyml-experimental"
     2.5    ML_PLATFORM="x86-darwin"
     2.6    ML_HOME="$POLYML_HOME/$ML_PLATFORM"
     2.7 -  ML_OPTIONS="--mutable 800 --immutable 2000"
     2.8 +  ML_OPTIONS="--mutable 600 --immutable 1800"
     2.9  
    2.10  
    2.11  ISABELLE_HOME_USER=~/isabelle-mac-poly-M4
    2.12 @@ -25,4 +25,4 @@
    2.13  
    2.14  ISABELLE_USEDIR_OPTIONS="-i false -d false -M 4"
    2.15  
    2.16 -HOL_USEDIR_OPTIONS="-p 2 -q 1"
    2.17 +HOL_USEDIR_OPTIONS="-p 2 -q 0"
     3.1 --- a/Admin/isatest/settings/mac-poly-M8	Wed Jul 22 10:49:26 2009 +0200
     3.2 +++ b/Admin/isatest/settings/mac-poly-M8	Wed Jul 22 11:23:09 2009 +0200
     3.3 @@ -25,4 +25,4 @@
     3.4  
     3.5  ISABELLE_USEDIR_OPTIONS="-i false -d false -M 8"
     3.6  
     3.7 -HOL_USEDIR_OPTIONS="-p 2 -q 1"
     3.8 +HOL_USEDIR_OPTIONS="-p 2 -q 0"
     4.1 --- a/NEWS	Wed Jul 22 10:49:26 2009 +0200
     4.2 +++ b/NEWS	Wed Jul 22 11:23:09 2009 +0200
     4.3 @@ -123,6 +123,11 @@
     4.4  cominators for "args".  INCOMPATIBILITY, need to use simplified
     4.5  Attrib/Method.setup introduced in Isabelle2009.
     4.6  
     4.7 +* Display.pretty_thm now requires a proper context (cf. former
     4.8 +ProofContext.pretty_thm).  May fall back on Display.pretty_thm_global
     4.9 +or even Display.pretty_thm_without_context as last resort.
    4.10 +INCOMPATIBILITY.
    4.11 +
    4.12  
    4.13  *** System ***
    4.14  
     5.1 --- a/src/FOLP/classical.ML	Wed Jul 22 10:49:26 2009 +0200
     5.2 +++ b/src/FOLP/classical.ML	Wed Jul 22 11:23:09 2009 +0200
     5.3 @@ -124,11 +124,11 @@
     5.4  val empty_cs = make_cs{safeIs=[], safeEs=[], hazIs=[], hazEs=[]};
     5.5  
     5.6  fun print_cs (CS{safeIs,safeEs,hazIs,hazEs,...}) =
     5.7 - (writeln"Introduction rules";  Display.prths hazIs;
     5.8 -  writeln"Safe introduction rules";  Display.prths safeIs;
     5.9 -  writeln"Elimination rules";  Display.prths hazEs;
    5.10 -  writeln"Safe elimination rules";  Display.prths safeEs;
    5.11 -  ());
    5.12 +  writeln (cat_lines
    5.13 +   (["Introduction rules"] @ map Display.string_of_thm_without_context hazIs @
    5.14 +    ["Safe introduction rules"] @ map Display.string_of_thm_without_context safeIs @
    5.15 +    ["Elimination rules"] @ map Display.string_of_thm_without_context hazEs @
    5.16 +    ["Safe elimination rules"] @ map Display.string_of_thm_without_context safeEs));
    5.17  
    5.18  fun (CS{safeIs,safeEs,hazIs,hazEs,...}) addSIs ths =
    5.19    make_cs {safeIs=ths@safeIs, safeEs=safeEs, hazIs=hazIs, hazEs=hazEs};
     6.1 --- a/src/FOLP/ex/Prolog.ML	Wed Jul 22 10:49:26 2009 +0200
     6.2 +++ b/src/FOLP/ex/Prolog.ML	Wed Jul 22 11:23:09 2009 +0200
     6.3 @@ -13,7 +13,7 @@
     6.4  by (resolve_tac [appNil,appCons] 1);
     6.5  by (resolve_tac [appNil,appCons] 1);
     6.6  by (resolve_tac [appNil,appCons] 1);
     6.7 -prth (result());
     6.8 +result();
     6.9  
    6.10  Goal "app(?x, c:d:Nil, a:b:c:d:Nil)";
    6.11  by (REPEAT (resolve_tac [appNil,appCons] 1));
     7.1 --- a/src/FOLP/simp.ML	Wed Jul 22 10:49:26 2009 +0200
     7.2 +++ b/src/FOLP/simp.ML	Wed Jul 22 11:23:09 2009 +0200
     7.3 @@ -113,7 +113,7 @@
     7.4    let fun norm thm = 
     7.5        case lhs_of(concl_of thm) of
     7.6            Const(n,_)$_ => n
     7.7 -        | _ => (Display.prths normE_thms; error"No constant in lhs of a norm_thm")
     7.8 +        | _ => error "No constant in lhs of a norm_thm"
     7.9    in map norm normE_thms end;
    7.10  
    7.11  fun lhs_is_NORM(thm,i) = case lhs_of_eq i thm of
    7.12 @@ -122,7 +122,7 @@
    7.13  val refl_tac = resolve_tac refl_thms;
    7.14  
    7.15  fun find_res thms thm =
    7.16 -    let fun find [] = (Display.prths thms; error"Check Simp_Data")
    7.17 +    let fun find [] = error "Check Simp_Data"
    7.18            | find(th::thms) = thm RS th handle THM _ => find thms
    7.19      in find thms end;
    7.20  
    7.21 @@ -249,8 +249,8 @@
    7.22  fun insert_thm_warn th net = 
    7.23    Net.insert_term Thm.eq_thm_prop (concl_of th, th) net
    7.24    handle Net.INSERT => 
    7.25 -    (writeln"\nDuplicate rewrite or congruence rule:"; Display.print_thm th;
    7.26 -     net);
    7.27 +    (writeln ("Duplicate rewrite or congruence rule:\n" ^
    7.28 +        Display.string_of_thm_without_context th); net);
    7.29  
    7.30  val insert_thms = fold_rev insert_thm_warn;
    7.31  
    7.32 @@ -275,8 +275,8 @@
    7.33  fun delete_thm_warn th net = 
    7.34    Net.delete_term Thm.eq_thm_prop (concl_of th, th) net
    7.35    handle Net.DELETE => 
    7.36 -    (writeln"\nNo such rewrite or congruence rule:";  Display.print_thm th;
    7.37 -     net);
    7.38 +    (writeln ("No such rewrite or congruence rule:\n" ^
    7.39 +        Display.string_of_thm_without_context th); net);
    7.40  
    7.41  val delete_thms = fold_rev delete_thm_warn;
    7.42  
    7.43 @@ -290,9 +290,9 @@
    7.44  fun delrew(SS{auto_tac,congs,cong_net,mk_simps,simps,simp_net}, thm) =
    7.45  let fun find((p as (th,ths))::ps',ps) =
    7.46            if Thm.eq_thm_prop(thm,th) then (ths,ps@ps') else find(ps',p::ps)
    7.47 -      | find([],simps') = (writeln"\nNo such rewrite or congruence rule:";
    7.48 -                           Display.print_thm thm;
    7.49 -                           ([],simps'))
    7.50 +      | find([],simps') =
    7.51 +          (writeln ("No such rewrite or congruence rule:\n" ^
    7.52 +              Display.string_of_thm_without_context thm); ([], simps'))
    7.53      val (thms,simps') = find(simps,[])
    7.54  in SS{auto_tac=auto_tac, congs=congs, cong_net=cong_net, mk_simps=mk_simps,
    7.55        simps = simps', simp_net = delete_thms thms simp_net }
    7.56 @@ -311,8 +311,9 @@
    7.57  fun dest_ss(SS{congs,simps,...}) = (congs, map #1 simps);
    7.58  
    7.59  fun print_ss(SS{congs,simps,...}) =
    7.60 -        (writeln"Congruences:"; Display.prths congs;
    7.61 -         writeln"Rewrite Rules:"; Display.prths (map #1 simps); ());
    7.62 +  writeln (cat_lines
    7.63 +   (["Congruences:"] @ map Display.string_of_thm_without_context congs @
    7.64 +    ["Rewrite Rules:"] @ map (Display.string_of_thm_without_context o #1) simps));
    7.65  
    7.66  
    7.67  (* Rewriting with conditionals *)
    7.68 @@ -435,7 +436,8 @@
    7.69          val rwrls = map mk_trans (List.concat(map mk_rew_rules thms));
    7.70          val anet' = List.foldr lhs_insert_thm anet rwrls
    7.71      in  if !tracing andalso not(null new_rws)
    7.72 -        then (writeln"Adding rewrites:";  Display.prths new_rws;  ())
    7.73 +        then writeln (cat_lines
    7.74 +          ("Adding rewrites:" :: map Display.string_of_thm_without_context new_rws))
    7.75          else ();
    7.76          (ss,thm,anet',anet::ats,cs) 
    7.77      end;
     8.1 --- a/src/HOL/Import/import.ML	Wed Jul 22 10:49:26 2009 +0200
     8.2 +++ b/src/HOL/Import/import.ML	Wed Jul 22 11:23:09 2009 +0200
     8.3 @@ -44,9 +44,9 @@
     8.4              val thm = equal_elim rew thm
     8.5              val prew = ProofKernel.rewrite_hol4_term prem thy
     8.6              val prem' = #2 (Logic.dest_equals (prop_of prew))
     8.7 -            val _ = message ("Import proved " ^ Display.string_of_thm thm)
     8.8 +            val _ = message ("Import proved " ^ Display.string_of_thm ctxt thm)
     8.9              val thm = ProofKernel.disambiguate_frees thm
    8.10 -            val _ = message ("Disambiguate: " ^ Display.string_of_thm thm)
    8.11 +            val _ = message ("Disambiguate: " ^ Display.string_of_thm ctxt thm)
    8.12          in
    8.13              case Shuffler.set_prop thy prem' [("",thm)] of
    8.14                  SOME (_,thm) =>
     9.1 --- a/src/HOL/Import/proof_kernel.ML	Wed Jul 22 10:49:26 2009 +0200
     9.2 +++ b/src/HOL/Import/proof_kernel.ML	Wed Jul 22 11:23:09 2009 +0200
     9.3 @@ -243,7 +243,7 @@
     9.4  
     9.5  val smart_string_of_thm = smart_string_of_cterm o cprop_of
     9.6  
     9.7 -fun prth th = writeln (PrintMode.setmp [] Display.string_of_thm th)
     9.8 +fun prth th = writeln (PrintMode.setmp [] Display.string_of_thm_without_context th)
     9.9  fun prc ct = writeln (PrintMode.setmp [] Display.string_of_cterm ct)
    9.10  fun prin t = writeln (PrintMode.setmp [] (fn () => Syntax.string_of_term_global (the_context ()) t) ());
    9.11  fun pth (HOLThm(ren,thm)) =
    10.1 --- a/src/HOL/Import/shuffler.ML	Wed Jul 22 10:49:26 2009 +0200
    10.2 +++ b/src/HOL/Import/shuffler.ML	Wed Jul 22 11:23:09 2009 +0200
    10.3 @@ -40,7 +40,7 @@
    10.4    case e of
    10.5       THM (msg,i,thms) =>
    10.6           (writeln ("Exception THM " ^ string_of_int i ^ " raised:\n" ^ msg);
    10.7 -          List.app Display.print_thm thms)
    10.8 +          List.app (writeln o Display.string_of_thm_global sign) thms)
    10.9     | THEORY (msg,thys) =>
   10.10           (writeln ("Exception THEORY raised:\n" ^ msg);
   10.11            List.app (writeln o Context.str_of_thy) thys)
   10.12 @@ -56,7 +56,7 @@
   10.13  (*Prints an exception, then fails*)
   10.14  fun print_sign_exn sign e = (print_sign_exn_unit sign e; raise e)
   10.15  
   10.16 -val string_of_thm = PrintMode.setmp [] Display.string_of_thm;
   10.17 +val string_of_thm = PrintMode.setmp [] Display.string_of_thm_without_context;
   10.18  val string_of_cterm = PrintMode.setmp [] Display.string_of_cterm;
   10.19  
   10.20  fun mk_meta_eq th =
   10.21 @@ -84,7 +84,7 @@
   10.22  
   10.23  fun print_shuffles thy =
   10.24    Pretty.writeln (Pretty.big_list "Shuffle theorems:"
   10.25 -    (map Display.pretty_thm (ShuffleData.get thy)))
   10.26 +    (map (Display.pretty_thm_global thy) (ShuffleData.get thy)))
   10.27  
   10.28  val weaken =
   10.29      let
    11.1 --- a/src/HOL/Nominal/nominal_thmdecls.ML	Wed Jul 22 10:49:26 2009 +0200
    11.2 +++ b/src/HOL/Nominal/nominal_thmdecls.ML	Wed Jul 22 11:23:09 2009 +0200
    11.3 @@ -156,7 +156,7 @@
    11.4        fold (fn thm => Data.map (flag thm)) thms_to_be_added context
    11.5    end
    11.6    handle EQVT_FORM s =>
    11.7 -      error (Display.string_of_thm orig_thm ^ 
    11.8 +      error (Display.string_of_thm (Context.proof_of context) orig_thm ^ 
    11.9                 " does not comply with the form of an equivariance lemma (" ^ s ^").")
   11.10  
   11.11  
    12.1 --- a/src/HOL/Tools/Function/lexicographic_order.ML	Wed Jul 22 10:49:26 2009 +0200
    12.2 +++ b/src/HOL/Tools/Function/lexicographic_order.ML	Wed Jul 22 11:23:09 2009 +0200
    12.3 @@ -140,7 +140,7 @@
    12.4  fun pr_table table = writeln (cat_lines (map (fn r => concat (map pr_cell r)) table))
    12.5  
    12.6  fun pr_goals ctxt st =
    12.7 -    Display.pretty_goals_aux (Syntax.pp ctxt) Markup.none (true, false) (Thm.nprems_of st) st
    12.8 +    Display_Goal.pretty_goals_aux (Syntax.pp ctxt) Markup.none (true, false) (Thm.nprems_of st) st
    12.9       |> Pretty.chunks
   12.10       |> Pretty.string_of
   12.11  
    13.1 --- a/src/HOL/Tools/TFL/casesplit.ML	Wed Jul 22 10:49:26 2009 +0200
    13.2 +++ b/src/HOL/Tools/TFL/casesplit.ML	Wed Jul 22 11:23:09 2009 +0200
    13.3 @@ -269,9 +269,9 @@
    13.4        fun split th =
    13.5            (case find_thms_split splitths 1 th of
    13.6               NONE =>
    13.7 -             (writeln "th:";
    13.8 -              Display.print_thm th; writeln "split ths:";
    13.9 -              Display.print_thms splitths; writeln "\n--";
   13.10 +             (writeln (cat_lines
   13.11 +              (["th:", Display.string_of_thm_without_context th, "split ths:"] @
   13.12 +                map Display.string_of_thm_without_context splitths @ ["\n--"]));
   13.13                error "splitto: cannot find variable to split on")
   13.14              | SOME v =>
   13.15               let
    14.1 --- a/src/HOL/Tools/TFL/rules.ML	Wed Jul 22 10:49:26 2009 +0200
    14.2 +++ b/src/HOL/Tools/TFL/rules.ML	Wed Jul 22 11:23:09 2009 +0200
    14.3 @@ -552,7 +552,7 @@
    14.4  fun say s = if !tracing then writeln s else ();
    14.5  
    14.6  fun print_thms s L =
    14.7 -  say (cat_lines (s :: map Display.string_of_thm L));
    14.8 +  say (cat_lines (s :: map Display.string_of_thm_without_context L));
    14.9  
   14.10  fun print_cterms s L =
   14.11    say (cat_lines (s :: map Display.string_of_cterm L));
   14.12 @@ -677,7 +677,7 @@
   14.13               val cntxt = Simplifier.prems_of_ss ss
   14.14               val dummy = print_thms "cntxt:" cntxt
   14.15               val dummy = say "cong rule:"
   14.16 -             val dummy = say (Display.string_of_thm thm)
   14.17 +             val dummy = say (Display.string_of_thm_without_context thm)
   14.18               val dummy = thm_ref := (thm :: !thm_ref)
   14.19               val dummy = ss_ref := (ss :: !ss_ref)
   14.20               (* Unquantified eliminate *)
    15.1 --- a/src/HOL/Tools/TFL/tfl.ML	Wed Jul 22 10:49:26 2009 +0200
    15.2 +++ b/src/HOL/Tools/TFL/tfl.ML	Wed Jul 22 11:23:09 2009 +0200
    15.3 @@ -529,9 +529,8 @@
    15.4       val f = #lhs(S.dest_eq proto_def)
    15.5       val (extractants,TCl) = ListPair.unzip extracta
    15.6       val dummy = if !trace
    15.7 -                 then (writeln "Extractants = ";
    15.8 -                       Display.prths extractants;
    15.9 -                       ())
   15.10 +                 then writeln (cat_lines ("Extractants =" ::
   15.11 +                  map (Display.string_of_thm_global thy) extractants))
   15.12                   else ()
   15.13       val TCs = List.foldr (gen_union (op aconv)) [] TCl
   15.14       val full_rqt = WFR::TCs
   15.15 @@ -551,8 +550,9 @@
   15.16         |> PureThy.add_defs false
   15.17              [Thm.no_attributes (Binding.name (fid ^ "_def"), defn)]
   15.18       val def = Thm.freezeT def0;
   15.19 -     val dummy = if !trace then writeln ("DEF = " ^ Display.string_of_thm def)
   15.20 -                           else ()
   15.21 +     val dummy =
   15.22 +       if !trace then writeln ("DEF = " ^ Display.string_of_thm_global theory def)
   15.23 +       else ()
   15.24       (* val fconst = #lhs(S.dest_eq(concl def))  *)
   15.25       val tych = Thry.typecheck theory
   15.26       val full_rqt_prop = map (Dcterm.mk_prop o tych) full_rqt
   15.27 @@ -560,7 +560,7 @@
   15.28       val baz = R.DISCH_ALL
   15.29                   (fold_rev R.DISCH full_rqt_prop
   15.30                    (R.LIST_CONJ extractants))
   15.31 -     val dum = if !trace then writeln ("baz = " ^ Display.string_of_thm baz)
   15.32 +     val dum = if !trace then writeln ("baz = " ^ Display.string_of_thm_global theory baz)
   15.33                             else ()
   15.34       val f_free = Free (fid, fastype_of f)  (*'cos f is a Const*)
   15.35       val SV' = map tych SV;
   15.36 @@ -909,7 +909,7 @@
   15.37  
   15.38  
   15.39  fun trace_thms s L =
   15.40 -  if !trace then writeln (cat_lines (s :: map Display.string_of_thm L))
   15.41 +  if !trace then writeln (cat_lines (s :: map Display.string_of_thm_without_context L))
   15.42    else ();
   15.43  
   15.44  fun trace_cterms s L =
    16.1 --- a/src/HOL/Tools/atp_minimal.ML	Wed Jul 22 10:49:26 2009 +0200
    16.2 +++ b/src/HOL/Tools/atp_minimal.ML	Wed Jul 22 11:23:09 2009 +0200
    16.3 @@ -125,7 +125,8 @@
    16.4        println ("Minimize called with " ^ length_string name_thms_pairs ^ " theorems, prover: "
    16.5          ^ prover_name ^ ", time limit: " ^ Int.toString time_limit ^ " seconds")
    16.6      val _ = debug_fn (fn () => app (fn (n, tl) =>
    16.7 -        (debug n; app (fn t => debug ("  " ^ Display.string_of_thm t)) tl)) name_thms_pairs)
    16.8 +        (debug n; app (fn t =>
    16.9 +          debug ("  " ^ Display.string_of_thm (Proof.context_of state) t)) tl)) name_thms_pairs)
   16.10      val test_thms_fun = sh_test_thms prover prover_name time_limit 1 state
   16.11      fun test_thms filtered thms =
   16.12        case test_thms_fun filtered thms of (Success _, _) => true | _ => false
    17.1 --- a/src/HOL/Tools/atp_wrapper.ML	Wed Jul 22 10:49:26 2009 +0200
    17.2 +++ b/src/HOL/Tools/atp_wrapper.ML	Wed Jul 22 11:23:09 2009 +0200
    17.3 @@ -62,7 +62,7 @@
    17.4      val goal_cls = #1 (ResAxioms.neg_conjecture_clauses th subgoalno)
    17.5        handle THM ("assume: variables", _, _) =>
    17.6          error "Sledgehammer: Goal contains type variables (TVars)"
    17.7 -    val _ = app (fn th => Output.debug (fn _ => Display.string_of_thm th)) goal_cls
    17.8 +    val _ = app (fn th => Output.debug (fn _ => Display.string_of_thm ctxt th)) goal_cls
    17.9      val the_filtered_clauses =
   17.10        case filtered_clauses of
   17.11            NONE => relevance_filter goal goal_cls
    18.1 --- a/src/HOL/Tools/choice_specification.ML	Wed Jul 22 10:49:26 2009 +0200
    18.2 +++ b/src/HOL/Tools/choice_specification.ML	Wed Jul 22 11:23:09 2009 +0200
    18.3 @@ -183,7 +183,7 @@
    18.4                          fun add_final (arg as (thy, thm)) =
    18.5                              if name = ""
    18.6                              then arg |> Library.swap
    18.7 -                            else (writeln ("  " ^ name ^ ": " ^ (Display.string_of_thm thm));
    18.8 +                            else (writeln ("  " ^ name ^ ": " ^ Display.string_of_thm_global thy thm);
    18.9                                    PureThy.store_thm (Binding.name name, thm) thy)
   18.10                      in
   18.11                          args |> apsnd (remove_alls frees)
    19.1 --- a/src/HOL/Tools/inductive.ML	Wed Jul 22 10:49:26 2009 +0200
    19.2 +++ b/src/HOL/Tools/inductive.ML	Wed Jul 22 11:23:09 2009 +0200
    19.3 @@ -140,7 +140,7 @@
    19.4      val space = Consts.space_of (ProofContext.consts_of ctxt);
    19.5    in
    19.6      [Pretty.strs ("(co)inductives:" :: map #1 (NameSpace.extern_table (space, tab))),
    19.7 -     Pretty.big_list "monotonicity rules:" (map (ProofContext.pretty_thm ctxt) monos)]
    19.8 +     Pretty.big_list "monotonicity rules:" (map (Display.pretty_thm ctxt) monos)]
    19.9      |> Pretty.chunks |> Pretty.writeln
   19.10    end;
   19.11  
   19.12 @@ -179,7 +179,8 @@
   19.13        [dest_less_concl (Seq.hd (REPEAT (FIRSTGOAL
   19.14           (resolve_tac [le_funI, le_boolI'])) thm))]
   19.15      | _ => [thm]
   19.16 -  end handle THM _ => error ("Bad monotonicity theorem:\n" ^ Display.string_of_thm thm);
   19.17 +  end handle THM _ =>
   19.18 +    error ("Bad monotonicity theorem:\n" ^ Display.string_of_thm_without_context thm);
   19.19  
   19.20  val mono_add = Thm.declaration_attribute (map_monos o fold Thm.add_thm o mk_mono);
   19.21  val mono_del = Thm.declaration_attribute (map_monos o fold Thm.del_thm o mk_mono);
    20.1 --- a/src/HOL/Tools/inductive_codegen.ML	Wed Jul 22 10:49:26 2009 +0200
    20.2 +++ b/src/HOL/Tools/inductive_codegen.ML	Wed Jul 22 11:23:09 2009 +0200
    20.3 @@ -39,7 +39,7 @@
    20.4  
    20.5  
    20.6  fun warn thm = warning ("InductiveCodegen: Not a proper clause:\n" ^
    20.7 -  Display.string_of_thm thm);
    20.8 +  Display.string_of_thm_without_context thm);
    20.9  
   20.10  fun add_node (g, x) = Graph.new_node (x, ()) g handle Graph.DUP _ => g;
   20.11  
    21.1 --- a/src/HOL/Tools/inductive_realizer.ML	Wed Jul 22 10:49:26 2009 +0200
    21.2 +++ b/src/HOL/Tools/inductive_realizer.ML	Wed Jul 22 11:23:09 2009 +0200
    21.3 @@ -19,7 +19,7 @@
    21.4    (case Proofterm.fold_proof_atoms false (fn PThm (_, ((name, _, _), _)) => cons name | _ => I)
    21.5        [Thm.proof_of thm] [] of
    21.6      [name] => name
    21.7 -  | _ => error ("name_of_thm: bad proof of theorem\n" ^ Display.string_of_thm thm));
    21.8 +  | _ => error ("name_of_thm: bad proof of theorem\n" ^ Display.string_of_thm_without_context thm));
    21.9  
   21.10  val all_simps = map (symmetric o mk_meta_eq) (thms "HOL.all_simps");
   21.11  
    22.1 --- a/src/HOL/Tools/lin_arith.ML	Wed Jul 22 10:49:26 2009 +0200
    22.2 +++ b/src/HOL/Tools/lin_arith.ML	Wed Jul 22 11:23:09 2009 +0200
    22.3 @@ -286,7 +286,7 @@
    22.4  
    22.5  (* checks if splitting with 'thm' is implemented                             *)
    22.6  
    22.7 -fun is_split_thm (thm : thm) : bool =
    22.8 +fun is_split_thm thm =
    22.9    case concl_of thm of _ $ (_ $ (_ $ lhs) $ _) => (
   22.10      (* Trueprop $ ((op =) $ (?P $ lhs) $ rhs) *)
   22.11      case head_of lhs of
   22.12 @@ -298,10 +298,10 @@
   22.13                                      "Divides.div_class.mod",
   22.14                                      "Divides.div_class.div"] a
   22.15      | _            => (warning ("Lin. Arith.: wrong format for split rule " ^
   22.16 -                                 Display.string_of_thm thm);
   22.17 +                                 Display.string_of_thm_without_context thm);
   22.18                         false))
   22.19    | _ => (warning ("Lin. Arith.: wrong format for split rule " ^
   22.20 -                   Display.string_of_thm thm);
   22.21 +                   Display.string_of_thm_without_context thm);
   22.22            false);
   22.23  
   22.24  (* substitute new for occurrences of old in a term, incrementing bound       *)
    23.1 --- a/src/HOL/Tools/meson.ML	Wed Jul 22 10:49:26 2009 +0200
    23.2 +++ b/src/HOL/Tools/meson.ML	Wed Jul 22 11:23:09 2009 +0200
    23.3 @@ -127,10 +127,10 @@
    23.4  fun forward_res nf st =
    23.5    let fun forward_tacf [prem] = rtac (nf prem) 1
    23.6          | forward_tacf prems =
    23.7 -            error ("Bad proof state in forward_res, please inform lcp@cl.cam.ac.uk:\n" ^
    23.8 -                   Display.string_of_thm st ^
    23.9 -                   "\nPremises:\n" ^
   23.10 -                   ML_Syntax.print_list Display.string_of_thm prems)
   23.11 +            error (cat_lines
   23.12 +              ("Bad proof state in forward_res, please inform lcp@cl.cam.ac.uk:" ::
   23.13 +                Display.string_of_thm_without_context st ::
   23.14 +                "Premises:" :: map Display.string_of_thm_without_context prems))
   23.15    in
   23.16      case Seq.pull (ALLGOALS (METAHYPS forward_tacf) st)
   23.17      of SOME(th,_) => th
   23.18 @@ -342,7 +342,7 @@
   23.19        and cnf_nil th = cnf_aux (th,[])
   23.20        val cls = 
   23.21  	    if too_many_clauses (SOME ctxt) (concl_of th)
   23.22 -	    then (warning ("cnf is ignoring: " ^ Display.string_of_thm th); ths)
   23.23 +	    then (warning ("cnf is ignoring: " ^ Display.string_of_thm ctxt th); ths)
   23.24  	    else cnf_aux (th,ths)
   23.25    in  (cls, !ctxtr)  end;
   23.26  
   23.27 @@ -545,7 +545,7 @@
   23.28    | skolemize_nnf_list (th::ths) = 
   23.29        skolemize th :: skolemize_nnf_list ths
   23.30        handle THM _ => (*RS can fail if Unify.search_bound is too small*)
   23.31 -       (warning ("Failed to Skolemize " ^ Display.string_of_thm th);
   23.32 +       (warning ("Failed to Skolemize " ^ Display.string_of_thm_without_context th);
   23.33          skolemize_nnf_list ths);
   23.34  
   23.35  fun add_clauses (th,cls) =
   23.36 @@ -628,19 +628,17 @@
   23.37      ITER_DEEPEN (has_fewer_prems 1) (prolog_step_tac' horns);
   23.38  
   23.39  fun iter_deepen_meson_tac ths = MESON make_clauses
   23.40 - (fn cls =>
   23.41 -      case (gocls (cls@ths)) of
   23.42 -           [] => no_tac  (*no goal clauses*)
   23.43 -         | goes =>
   23.44 -             let val horns = make_horns (cls@ths)
   23.45 -                 val _ =
   23.46 -                     Output.debug (fn () => ("meson method called:\n" ^
   23.47 -                                  ML_Syntax.print_list Display.string_of_thm (cls@ths) ^
   23.48 -                                  "\nclauses:\n" ^
   23.49 -                                  ML_Syntax.print_list Display.string_of_thm horns))
   23.50 -             in THEN_ITER_DEEPEN (resolve_tac goes 1) (has_fewer_prems 1) (prolog_step_tac' horns)
   23.51 -             end
   23.52 - );
   23.53 +  (fn cls =>
   23.54 +    (case (gocls (cls @ ths)) of
   23.55 +      [] => no_tac  (*no goal clauses*)
   23.56 +    | goes =>
   23.57 +        let
   23.58 +          val horns = make_horns (cls @ ths)
   23.59 +          val _ = Output.debug (fn () =>
   23.60 +            cat_lines ("meson method called:" ::
   23.61 +              map Display.string_of_thm_without_context (cls @ ths) @
   23.62 +              ["clauses:"] @ map Display.string_of_thm_without_context horns))
   23.63 +        in THEN_ITER_DEEPEN (resolve_tac goes 1) (has_fewer_prems 1) (prolog_step_tac' horns) end));
   23.64  
   23.65  fun meson_claset_tac ths cs =
   23.66    SELECT_GOAL (TRY (safe_tac cs) THEN TRYALL (iter_deepen_meson_tac ths));
    24.1 --- a/src/HOL/Tools/metis_tools.ML	Wed Jul 22 10:49:26 2009 +0200
    24.2 +++ b/src/HOL/Tools/metis_tools.ML	Wed Jul 22 11:23:09 2009 +0200
    24.3 @@ -270,7 +270,7 @@
    24.4    fun print_thpair (fth,th) =
    24.5      (Output.debug (fn () => "=============================================");
    24.6       Output.debug (fn () => "Metis: " ^ Metis.Thm.toString fth);
    24.7 -     Output.debug (fn () => "Isabelle: " ^ Display.string_of_thm th));
    24.8 +     Output.debug (fn () => "Isabelle: " ^ Display.string_of_thm_without_context th));
    24.9  
   24.10    fun lookth thpairs (fth : Metis.Thm.thm) =
   24.11      valOf (AList.lookup (uncurry Metis.Thm.equal) thpairs fth)
   24.12 @@ -310,7 +310,7 @@
   24.13                in  SOME (cterm_of thy (Var v), t)  end
   24.14                handle Option =>
   24.15                    (Output.debug (fn() => "List.find failed for the variable " ^ x ^
   24.16 -                                         " in " ^ Display.string_of_thm i_th);
   24.17 +                                         " in " ^ Display.string_of_thm ctxt i_th);
   24.18                     NONE)
   24.19          fun remove_typeinst (a, t) =
   24.20                case Recon.strip_prefix ResClause.schematic_var_prefix a of
   24.21 @@ -318,7 +318,7 @@
   24.22                  | NONE   => case Recon.strip_prefix ResClause.tvar_prefix a of
   24.23                    SOME _ => NONE          (*type instantiations are forbidden!*)
   24.24                  | NONE   => SOME (a,t)    (*internal Metis var?*)
   24.25 -        val _ = Output.debug (fn () => "  isa th: " ^ Display.string_of_thm i_th)
   24.26 +        val _ = Output.debug (fn () => "  isa th: " ^ Display.string_of_thm ctxt i_th)
   24.27          val substs = List.mapPartial remove_typeinst (Metis.Subst.toList fsubst)
   24.28          val (vars,rawtms) = ListPair.unzip (List.mapPartial subst_translation substs)
   24.29          val tms = infer_types ctxt rawtms;
   24.30 @@ -350,8 +350,8 @@
   24.31      let
   24.32        val thy = ProofContext.theory_of ctxt
   24.33        val i_th1 = lookth thpairs th1 and i_th2 = lookth thpairs th2
   24.34 -      val _ = Output.debug (fn () => "  isa th1 (pos): " ^ Display.string_of_thm i_th1)
   24.35 -      val _ = Output.debug (fn () => "  isa th2 (neg): " ^ Display.string_of_thm i_th2)
   24.36 +      val _ = Output.debug (fn () => "  isa th1 (pos): " ^ Display.string_of_thm ctxt i_th1)
   24.37 +      val _ = Output.debug (fn () => "  isa th2 (neg): " ^ Display.string_of_thm ctxt i_th2)
   24.38      in
   24.39        if is_TrueI i_th1 then i_th2 (*Trivial cases where one operand is type info*)
   24.40        else if is_TrueI i_th2 then i_th1
   24.41 @@ -428,7 +428,7 @@
   24.42          val _ = Output.debug (fn () => "located term: " ^ Syntax.string_of_term ctxt tm_subst)
   24.43          val imax = maxidx_of_term (i_tm $ tm_abs $ tm_subst)  (*ill typed but gives right max*)
   24.44          val subst' = incr_indexes (imax+1) (if pos then subst_em else ssubst_em)
   24.45 -        val _ = Output.debug (fn () => "subst' " ^ Display.string_of_thm subst')
   24.46 +        val _ = Output.debug (fn () => "subst' " ^ Display.string_of_thm ctxt subst')
   24.47          val eq_terms = map (pairself (cterm_of thy))
   24.48                             (ListPair.zip (OldTerm.term_vars (prop_of subst'), [tm_abs, tm_subst, i_tm]))
   24.49      in  cterm_instantiate eq_terms subst'  end;
   24.50 @@ -456,7 +456,7 @@
   24.51              val _ = Output.debug (fn () => "METIS THM: " ^ Metis.Thm.toString fol_th)
   24.52              val _ = Output.debug (fn () => "INFERENCE: " ^ Metis.Proof.inferenceToString inf)
   24.53              val th = Meson.flexflex_first_order (step ctxt isFO thpairs (fol_th, inf))
   24.54 -            val _ = Output.debug (fn () => "ISABELLE THM: " ^ Display.string_of_thm th)
   24.55 +            val _ = Output.debug (fn () => "ISABELLE THM: " ^ Display.string_of_thm ctxt th)
   24.56              val _ = Output.debug (fn () => "=============================================")
   24.57              val n_metis_lits = length (filter real_literal (Metis.LiteralSet.toList (Metis.Thm.clause fol_th)))
   24.58          in
   24.59 @@ -576,9 +576,9 @@
   24.60          val th_cls_pairs = map (fn th => (Thm.get_name_hint th, ResAxioms.cnf_axiom thy th)) ths0
   24.61          val ths = List.concat (map #2 th_cls_pairs)
   24.62          val _ = Output.debug (fn () => "FOL_SOLVE: CONJECTURE CLAUSES")
   24.63 -        val _ = app (fn th => Output.debug (fn () => Display.string_of_thm th)) cls
   24.64 +        val _ = app (fn th => Output.debug (fn () => Display.string_of_thm ctxt th)) cls
   24.65          val _ = Output.debug (fn () => "THEOREM CLAUSES")
   24.66 -        val _ = app (fn th => Output.debug (fn () => Display.string_of_thm th)) ths
   24.67 +        val _ = app (fn th => Output.debug (fn () => Display.string_of_thm ctxt th)) ths
   24.68          val {isFO,axioms,tfrees} = build_map mode ctxt cls ths
   24.69          val _ = if null tfrees then ()
   24.70                  else (Output.debug (fn () => "TFREE CLAUSES");
   24.71 @@ -604,14 +604,14 @@
   24.72                    val result = translate isFO ctxt' axioms proof
   24.73                    and used = List.mapPartial (used_axioms axioms) proof
   24.74                    val _ = Output.debug (fn () => "METIS COMPLETED...clauses actually used:")
   24.75 -	          val _ = app (fn th => Output.debug (fn () => Display.string_of_thm th)) used
   24.76 +	          val _ = app (fn th => Output.debug (fn () => Display.string_of_thm ctxt th)) used
   24.77  	          val unused = filter (fn (a,cls) => not (common_thm used cls)) th_cls_pairs
   24.78                in
   24.79                    if null unused then ()
   24.80                    else warning ("Metis: unused theorems " ^ commas_quote (map #1 unused));
   24.81                    case result of
   24.82                        (_,ith)::_ => 
   24.83 -                          (Output.debug (fn () => "success: " ^ Display.string_of_thm ith); 
   24.84 +                          (Output.debug (fn () => "success: " ^ Display.string_of_thm ctxt ith); 
   24.85                             [ith])
   24.86                      | _ => (Output.debug (fn () => "Metis: no result"); 
   24.87                              [])
   24.88 @@ -623,7 +623,7 @@
   24.89  
   24.90    fun metis_general_tac mode ctxt ths i st0 =
   24.91      let val _ = Output.debug (fn () =>
   24.92 -          "Metis called with theorems " ^ cat_lines (map Display.string_of_thm ths))
   24.93 +          "Metis called with theorems " ^ cat_lines (map (Display.string_of_thm ctxt) ths))
   24.94      in
   24.95         if exists_type ResAxioms.type_has_empty_sort (prop_of st0)  
   24.96         then (warning "Proof state contains the empty sort"; Seq.empty)
    25.1 --- a/src/HOL/Tools/recdef.ML	Wed Jul 22 10:49:26 2009 +0200
    25.2 +++ b/src/HOL/Tools/recdef.ML	Wed Jul 22 11:23:09 2009 +0200
    25.3 @@ -48,9 +48,9 @@
    25.4  fun map_wfs f = map_hints (fn (simps, congs, wfs) => (simps, congs, f wfs));
    25.5  
    25.6  fun pretty_hints ({simps, congs, wfs}: hints) =
    25.7 - [Pretty.big_list "recdef simp hints:" (map Display.pretty_thm simps),
    25.8 -  Pretty.big_list "recdef cong hints:" (map Display.pretty_thm (map snd congs)),
    25.9 -  Pretty.big_list "recdef wf hints:" (map Display.pretty_thm wfs)];
   25.10 + [Pretty.big_list "recdef simp hints:" (map Display.pretty_thm_without_context simps),
   25.11 +  Pretty.big_list "recdef cong hints:" (map Display.pretty_thm_without_context (map snd congs)),
   25.12 +  Pretty.big_list "recdef wf hints:" (map Display.pretty_thm_without_context wfs)];
   25.13  
   25.14  
   25.15  (* congruence rules *)
    26.1 --- a/src/HOL/Tools/record.ML	Wed Jul 22 10:49:26 2009 +0200
    26.2 +++ b/src/HOL/Tools/record.ML	Wed Jul 22 11:23:09 2009 +0200
    26.3 @@ -105,7 +105,7 @@
    26.4  (* messages *)
    26.5  
    26.6  fun trace_thm str thm =
    26.7 -    tracing (str ^ (Pretty.string_of (Display.pretty_thm thm)));
    26.8 +    tracing (str ^ (Pretty.string_of (Display.pretty_thm_without_context thm)));
    26.9  
   26.10  fun trace_thms str thms =
   26.11      (tracing str; map (trace_thm "") thms);
    27.1 --- a/src/HOL/Tools/res_atp.ML	Wed Jul 22 10:49:26 2009 +0200
    27.2 +++ b/src/HOL/Tools/res_atp.ML	Wed Jul 22 11:23:09 2009 +0200
    27.3 @@ -401,8 +401,9 @@
    27.4          (List.foldl add_single_names (List.foldl add_multi_names [] mults) singles)
    27.5    end;
    27.6  
    27.7 -fun check_named ("",th) = (warning ("No name for theorem " ^ Display.string_of_thm th); false)
    27.8 -  | check_named (_,th) = true;
    27.9 +fun check_named ("", th) =
   27.10 +      (warning ("No name for theorem " ^ Display.string_of_thm_without_context th); false)
   27.11 +  | check_named (_, th) = true;
   27.12  
   27.13  (* get lemmas from claset, simpset, atpset and extra supplied rules *)
   27.14  fun get_clasimp_atp_lemmas ctxt =
   27.15 @@ -538,7 +539,7 @@
   27.16      val extra_cls = white_cls @ extra_cls
   27.17      val axcls = white_cls @ axcls
   27.18      val ccls = subtract_cls goal_cls extra_cls
   27.19 -    val _ = app (fn th => Output.debug (fn _ => Display.string_of_thm th)) ccls
   27.20 +    val _ = app (fn th => Output.debug (fn _ => Display.string_of_thm_global thy th)) ccls
   27.21      val ccltms = map prop_of ccls
   27.22      and axtms = map (prop_of o #1) extra_cls
   27.23      val subs = tfree_classes_of_terms ccltms
    28.1 --- a/src/HOL/Tools/res_axioms.ML	Wed Jul 22 10:49:26 2009 +0200
    28.2 +++ b/src/HOL/Tools/res_axioms.ML	Wed Jul 22 11:23:09 2009 +0200
    28.3 @@ -227,8 +227,9 @@
    28.4          val eqth = combinators_aux (cprop_of th)
    28.5      in  equal_elim eqth th   end
    28.6      handle THM (msg,_,_) =>
    28.7 -      (warning ("Error in the combinator translation of " ^ Display.string_of_thm th);
    28.8 -       warning ("  Exception message: " ^ msg);
    28.9 +      (warning (cat_lines
   28.10 +        ["Error in the combinator translation of " ^ Display.string_of_thm_without_context th,
   28.11 +          "  Exception message: " ^ msg]);
   28.12         TrueI);  (*A type variable of sort {} will cause make abstraction fail.*)
   28.13  
   28.14  (*cterms are used throughout for efficiency*)
   28.15 @@ -280,7 +281,7 @@
   28.16  fun assert_lambda_free ths msg =
   28.17    case filter (not o lambda_free o prop_of) ths of
   28.18        [] => ()
   28.19 -    | ths' => error (msg ^ "\n" ^ cat_lines (map Display.string_of_thm ths'));
   28.20 +    | ths' => error (cat_lines (msg :: map Display.string_of_thm_without_context ths'));
   28.21  
   28.22  
   28.23  (*** Blacklisting (duplicated in ResAtp?) ***)
   28.24 @@ -336,7 +337,7 @@
   28.25  
   28.26  fun name_or_string th =
   28.27    if Thm.has_name_hint th then Thm.get_name_hint th
   28.28 -  else Display.string_of_thm th;
   28.29 +  else Display.string_of_thm_without_context th;
   28.30  
   28.31  (*Skolemize a named theorem, with Skolem functions as additional premises.*)
   28.32  fun skolem_thm (s, th) =
    29.1 --- a/src/HOL/Tools/res_reconstruct.ML	Wed Jul 22 10:49:26 2009 +0200
    29.2 +++ b/src/HOL/Tools/res_reconstruct.ML	Wed Jul 22 11:23:09 2009 +0200
    29.3 @@ -31,7 +31,7 @@
    29.4  fun trace s = if !Output.debugging then File.append (File.tmp_path trace_path) s
    29.5                else ();
    29.6  
    29.7 -val string_of_thm = PrintMode.setmp [] Display.string_of_thm;
    29.8 +fun string_of_thm ctxt = PrintMode.setmp [] (Display.string_of_thm ctxt);
    29.9  
   29.10  (*For generating structured proofs: keep every nth proof line*)
   29.11  val (modulus, modulus_setup) = Attrib.config_int "sledgehammer_modulus" 1;
   29.12 @@ -445,8 +445,9 @@
   29.13        val (ccls,fixes) = ResAxioms.neg_conjecture_clauses th sgno
   29.14        val _ = trace (Int.toString (length ccls) ^ " conjecture clauses\n")
   29.15        val ccls = map forall_intr_vars ccls
   29.16 -      val _ = if !Output.debugging then app (fn th => trace ("\nccl: " ^ string_of_thm th)) ccls
   29.17 -              else ()
   29.18 +      val _ =
   29.19 +        if !Output.debugging then app (fn th => trace ("\nccl: " ^ string_of_thm ctxt th)) ccls
   29.20 +        else ()
   29.21        val ilines = isar_lines ctxt (map prop_of ccls) (stringify_deps thm_names [] lines)
   29.22        val _ = trace "\ndecode_tstp_file: finishing\n"
   29.23    in
    30.1 --- a/src/HOL/Tools/sat_funcs.ML	Wed Jul 22 10:49:26 2009 +0200
    30.2 +++ b/src/HOL/Tools/sat_funcs.ML	Wed Jul 22 11:23:09 2009 +0200
    30.3 @@ -119,7 +119,7 @@
    30.4  (* (Thm.thm * (int * Thm.cterm) list) list -> Thm.thm * (int * Thm.cterm) list *)
    30.5  
    30.6  fun resolve_raw_clauses [] =
    30.7 -	raise THM ("Proof reconstruction failed (empty list of resolvents)!", 0, [])
    30.8 +      raise THM ("Proof reconstruction failed (empty list of resolvents)!", 0, [])
    30.9    | resolve_raw_clauses (c::cs) =
   30.10  	let
   30.11  		(* merges two sorted lists wrt. 'lit_ord', suppressing duplicates *)
   30.12 @@ -134,9 +134,9 @@
   30.13  		(* find out which two hyps are used in the resolution *)
   30.14  		(* (int * Thm.cterm) list * (int * Thm.cterm) list -> (int * Thm.cterm) list -> bool * Thm.cterm * Thm.cterm * (int * Thm.cterm) list *)
   30.15  		fun find_res_hyps ([], _) _ =
   30.16 -			raise THM ("Proof reconstruction failed (no literal for resolution)!", 0, [])
   30.17 +          raise THM ("Proof reconstruction failed (no literal for resolution)!", 0, [])
   30.18  		  | find_res_hyps (_, []) _ =
   30.19 -			raise THM ("Proof reconstruction failed (no literal for resolution)!", 0, [])
   30.20 +          raise THM ("Proof reconstruction failed (no literal for resolution)!", 0, [])
   30.21  		  | find_res_hyps (h1 :: hyps1, h2 :: hyps2) acc =
   30.22  			(case (lit_ord o pairself fst) (h1, h2) of
   30.23  			  LESS  => find_res_hyps (hyps1, h2 :: hyps2) (h1 :: acc)
   30.24 @@ -154,9 +154,12 @@
   30.25  		(* Thm.thm * (int * Thm.cterm) list -> Thm.thm * (int * Thm.cterm) list -> Thm.thm * (int * Thm.cterm) list *)
   30.26  		fun resolution (c1, hyps1) (c2, hyps2) =
   30.27  		let
   30.28 -			val _ = if !trace_sat then
   30.29 -					tracing ("Resolving clause: " ^ Display.string_of_thm c1 ^ " (hyps: " ^ ML_Syntax.print_list (Syntax.string_of_term_global (theory_of_thm c1)) (#hyps (rep_thm c1))
   30.30 -						^ ")\nwith clause: " ^ Display.string_of_thm c2 ^ " (hyps: " ^ ML_Syntax.print_list (Syntax.string_of_term_global (theory_of_thm c2)) (#hyps (rep_thm c2)) ^ ")")
   30.31 +			val _ =
   30.32 +			  if ! trace_sat then
   30.33 +					tracing ("Resolving clause: " ^ Display.string_of_thm_without_context c1 ^
   30.34 +					  " (hyps: " ^ ML_Syntax.print_list (Syntax.string_of_term_global (theory_of_thm c1)) (#hyps (rep_thm c1))
   30.35 +						^ ")\nwith clause: " ^ Display.string_of_thm_without_context c2 ^
   30.36 +						" (hyps: " ^ ML_Syntax.print_list (Syntax.string_of_term_global (theory_of_thm c2)) (#hyps (rep_thm c2)) ^ ")")
   30.37  				else ()
   30.38  
   30.39  			(* the two literals used for resolution *)
   30.40 @@ -172,8 +175,9 @@
   30.41  					Thm.instantiate ([], [(cP, cLit)]) resolution_thm
   30.42  				end
   30.43  
   30.44 -			val _ = if !trace_sat then
   30.45 -					tracing ("Resolution theorem: " ^ Display.string_of_thm res_thm)
   30.46 +			val _ =
   30.47 +			  if !trace_sat then
   30.48 +					tracing ("Resolution theorem: " ^ Display.string_of_thm_without_context res_thm)
   30.49  				else ()
   30.50  
   30.51  			(* Gamma1, Gamma2 |- False *)
   30.52 @@ -181,8 +185,11 @@
   30.53  				(Thm.implies_elim res_thm (if hyp1_is_neg then c2' else c1'))
   30.54  				(if hyp1_is_neg then c1' else c2')
   30.55  
   30.56 -			val _ = if !trace_sat then
   30.57 -					tracing ("Resulting clause: " ^ Display.string_of_thm c_new ^ " (hyps: " ^ ML_Syntax.print_list (Syntax.string_of_term_global (theory_of_thm c_new)) (#hyps (rep_thm c_new)) ^ ")")
   30.58 +			val _ =
   30.59 +			  if !trace_sat then
   30.60 +					tracing ("Resulting clause: " ^ Display.string_of_thm_without_context c_new ^
   30.61 +					  " (hyps: " ^ ML_Syntax.print_list
   30.62 +					      (Syntax.string_of_term_global (theory_of_thm c_new)) (#hyps (rep_thm c_new)) ^ ")")
   30.63  				else ()
   30.64  			val _ = inc counter
   30.65  		in
    31.1 --- a/src/HOL/ex/ROOT.ML	Wed Jul 22 10:49:26 2009 +0200
    31.2 +++ b/src/HOL/ex/ROOT.ML	Wed Jul 22 11:23:09 2009 +0200
    31.3 @@ -83,6 +83,7 @@
    31.4  (* requires a proof-generating SAT solver (zChaff or MiniSAT) to be *)
    31.5  (* installed:                                                       *)
    31.6  try use_thy "SAT_Examples";
    31.7 +Future.shutdown ();
    31.8  
    31.9  (* requires zChaff (or some other reasonably fast SAT solver) to be *)
   31.10  (* installed:                                                       *)
    32.1 --- a/src/HOL/ex/predicate_compile.ML	Wed Jul 22 10:49:26 2009 +0200
    32.2 +++ b/src/HOL/ex/predicate_compile.ML	Wed Jul 22 11:23:09 2009 +0200
    32.3 @@ -236,11 +236,11 @@
    32.4        val _ = writeln ("predicate: " ^ pred)
    32.5        val _ = writeln ("number of parameters: " ^ string_of_int (nparams_of thy pred))
    32.6        val _ = writeln ("introrules: ")
    32.7 -      val _ = fold (fn thm => fn u =>  writeln (Display.string_of_thm thm))
    32.8 +      val _ = fold (fn thm => fn u => writeln (Display.string_of_thm_global thy thm))
    32.9          (rev (intros_of thy pred)) ()
   32.10      in
   32.11        if (has_elim thy pred) then
   32.12 -        writeln ("elimrule: " ^ Display.string_of_thm (the_elim_of thy pred))
   32.13 +        writeln ("elimrule: " ^ Display.string_of_thm_global thy (the_elim_of thy pred))
   32.14        else
   32.15          writeln ("no elimrule defined")
   32.16      end
    33.1 --- a/src/Provers/Arith/fast_lin_arith.ML	Wed Jul 22 10:49:26 2009 +0200
    33.2 +++ b/src/Provers/Arith/fast_lin_arith.ML	Wed Jul 22 11:23:09 2009 +0200
    33.3 @@ -417,8 +417,8 @@
    33.4  (* Translate back a proof.                                                   *)
    33.5  (* ------------------------------------------------------------------------- *)
    33.6  
    33.7 -fun trace_thm msg th =
    33.8 -  (if !trace then (tracing msg; tracing (Display.string_of_thm th)) else (); th);
    33.9 +fun trace_thm ctxt msg th =
   33.10 +  (if !trace then (tracing msg; tracing (Display.string_of_thm ctxt th)) else (); th);
   33.11  
   33.12  fun trace_term ctxt msg t =
   33.13    (if !trace then tracing (cat_lines [msg, Syntax.string_of_term ctxt t]) else (); t)
   33.14 @@ -472,7 +472,7 @@
   33.15              NONE =>
   33.16                (the (try_add ([thm2] RL inj_thms) thm1)
   33.17                  handle Option =>
   33.18 -                  (trace_thm "" thm1; trace_thm "" thm2;
   33.19 +                  (trace_thm ctxt "" thm1; trace_thm ctxt "" thm2;
   33.20                     sys_error "Linear arithmetic: failed to add thms"))
   33.21            | SOME thm => thm)
   33.22        | SOME thm => thm);
   33.23 @@ -511,24 +511,25 @@
   33.24        else mult n thm;
   33.25  
   33.26      fun simp thm =
   33.27 -      let val thm' = trace_thm "Simplified:" (full_simplify simpset' thm)
   33.28 +      let val thm' = trace_thm ctxt "Simplified:" (full_simplify simpset' thm)
   33.29        in if LA_Logic.is_False thm' then raise FalseE thm' else thm' end;
   33.30  
   33.31 -    fun mk (Asm i) = trace_thm ("Asm " ^ string_of_int i) (nth asms i)
   33.32 -      | mk (Nat i) = trace_thm ("Nat " ^ string_of_int i) (LA_Logic.mk_nat_thm thy (nth atoms i))
   33.33 -      | mk (LessD j)            = trace_thm "L" (hd ([mk j] RL lessD))
   33.34 -      | mk (NotLeD j)           = trace_thm "NLe" (mk j RS LA_Logic.not_leD)
   33.35 -      | mk (NotLeDD j)          = trace_thm "NLeD" (hd ([mk j RS LA_Logic.not_leD] RL lessD))
   33.36 -      | mk (NotLessD j)         = trace_thm "NL" (mk j RS LA_Logic.not_lessD)
   33.37 -      | mk (Added (j1, j2))     = simp (trace_thm "+" (add_thms (mk j1) (mk j2)))
   33.38 -      | mk (Multiplied (n, j))  = (trace_msg ("*" ^ string_of_int n); trace_thm "*" (mult_thm (n, mk j)))
   33.39 +    fun mk (Asm i) = trace_thm ctxt ("Asm " ^ string_of_int i) (nth asms i)
   33.40 +      | mk (Nat i) = trace_thm ctxt ("Nat " ^ string_of_int i) (LA_Logic.mk_nat_thm thy (nth atoms i))
   33.41 +      | mk (LessD j) = trace_thm ctxt "L" (hd ([mk j] RL lessD))
   33.42 +      | mk (NotLeD j) = trace_thm ctxt "NLe" (mk j RS LA_Logic.not_leD)
   33.43 +      | mk (NotLeDD j) = trace_thm ctxt "NLeD" (hd ([mk j RS LA_Logic.not_leD] RL lessD))
   33.44 +      | mk (NotLessD j) = trace_thm ctxt "NL" (mk j RS LA_Logic.not_lessD)
   33.45 +      | mk (Added (j1, j2)) = simp (trace_thm ctxt "+" (add_thms (mk j1) (mk j2)))
   33.46 +      | mk (Multiplied (n, j)) =
   33.47 +          (trace_msg ("*" ^ string_of_int n); trace_thm ctxt "*" (mult_thm (n, mk j)))
   33.48  
   33.49    in
   33.50      let
   33.51        val _ = trace_msg "mkthm";
   33.52 -      val thm = trace_thm "Final thm:" (mk just);
   33.53 +      val thm = trace_thm ctxt "Final thm:" (mk just);
   33.54        val fls = simplify simpset' thm;
   33.55 -      val _ = trace_thm "After simplification:" fls;
   33.56 +      val _ = trace_thm ctxt "After simplification:" fls;
   33.57        val _ =
   33.58          if LA_Logic.is_False fls then ()
   33.59          else
   33.60 @@ -536,15 +537,15 @@
   33.61              if count > warning_count_max then ()
   33.62              else
   33.63                (tracing (cat_lines
   33.64 -                (["Assumptions:"] @ map Display.string_of_thm asms @ [""] @
   33.65 -                 ["Proved:", Display.string_of_thm fls, ""] @
   33.66 +                (["Assumptions:"] @ map (Display.string_of_thm ctxt) asms @ [""] @
   33.67 +                 ["Proved:", Display.string_of_thm ctxt fls, ""] @
   33.68                   (if count <> warning_count_max then []
   33.69                    else ["\n(Reached maximal message count -- disabling future warnings)"])));
   33.70                  warning "Linear arithmetic should have refuted the assumptions.\n\
   33.71                    \Please inform Tobias Nipkow (nipkow@in.tum.de).")
   33.72            end;
   33.73      in fls end
   33.74 -    handle FalseE thm => trace_thm "False reached early:" thm
   33.75 +    handle FalseE thm => trace_thm ctxt "False reached early:" thm
   33.76    end;
   33.77  
   33.78  end;
   33.79 @@ -775,8 +776,9 @@
   33.80    fn state =>
   33.81      let
   33.82        val ctxt = Simplifier.the_context ss;
   33.83 -      val _ = trace_thm ("refute_tac (on subgoal " ^ string_of_int i ^ ", with " ^
   33.84 -                             string_of_int (length justs) ^ " justification(s)):") state
   33.85 +      val _ = trace_thm ctxt
   33.86 +        ("refute_tac (on subgoal " ^ string_of_int i ^ ", with " ^
   33.87 +          string_of_int (length justs) ^ " justification(s)):") state
   33.88        val {neqE, ...} = get_data ctxt;
   33.89        fun just1 j =
   33.90          (* eliminate inequalities *)
   33.91 @@ -784,7 +786,7 @@
   33.92            REPEAT_DETERM (eresolve_tac neqE i)
   33.93          else
   33.94            all_tac) THEN
   33.95 -          PRIMITIVE (trace_thm "State after neqE:") THEN
   33.96 +          PRIMITIVE (trace_thm ctxt "State after neqE:") THEN
   33.97            (* use theorems generated from the actual justifications *)
   33.98            METAHYPS (fn asms => rtac (mkthm ss asms j) 1) i
   33.99      in
  33.100 @@ -792,7 +794,7 @@
  33.101        DETERM (resolve_tac [LA_Logic.notI, LA_Logic.ccontr] i) THEN
  33.102        (* user-defined preprocessing of the subgoal *)
  33.103        DETERM (LA_Data.pre_tac ctxt i) THEN
  33.104 -      PRIMITIVE (trace_thm "State after pre_tac:") THEN
  33.105 +      PRIMITIVE (trace_thm ctxt "State after pre_tac:") THEN
  33.106        (* prove every resulting subgoal, using its justification *)
  33.107        EVERY (map just1 justs)
  33.108      end  state;
  33.109 @@ -881,7 +883,7 @@
  33.110      val (Falsethm, _) = fwdproof ss tree js
  33.111      val contr = if pos then LA_Logic.ccontr else LA_Logic.notI
  33.112      val concl = implies_intr cnTconcl Falsethm COMP contr
  33.113 -  in SOME (trace_thm "Proved by lin. arith. prover:" (LA_Logic.mk_Eq concl)) end
  33.114 +  in SOME (trace_thm ctxt "Proved by lin. arith. prover:" (LA_Logic.mk_Eq concl)) end
  33.115    (*in case concl contains ?-var, which makes assume fail:*)   (* FIXME Variable.import_terms *)
  33.116    handle THM _ => NONE;
  33.117  
    34.1 --- a/src/Provers/blast.ML	Wed Jul 22 10:49:26 2009 +0200
    34.2 +++ b/src/Provers/blast.ML	Wed Jul 22 11:23:09 2009 +0200
    34.3 @@ -492,7 +492,9 @@
    34.4  end;
    34.5  
    34.6  
    34.7 -fun TRACE rl tac st i = if !trace then (Display.prth rl; tac st i) else tac st i;
    34.8 +fun TRACE rl tac st i =
    34.9 +  if !trace then (writeln (Display.string_of_thm_without_context rl); tac st i)
   34.10 +  else tac st i;
   34.11  
   34.12  (*Resolution/matching tactics: if upd then the proof state may be updated.
   34.13    Matching makes the tactics more deterministic in the presence of Vars.*)
   34.14 @@ -509,14 +511,16 @@
   34.15          THEN
   34.16          rot_subgoals_tac (rot, #2 trl) i
   34.17    in Option.SOME (trl, tac) end
   34.18 -  handle ElimBadPrem => (*reject: prems don't preserve conclusion*)
   34.19 -            (warning("Ignoring weak elimination rule\n" ^ Display.string_of_thm rl);
   34.20 -             Option.NONE)
   34.21 -       | ElimBadConcl => (*ignore: conclusion is not just a variable*)
   34.22 -           (if !trace then (warning("Ignoring ill-formed elimination rule:\n" ^
   34.23 -                       "conclusion should be a variable\n" ^ Display.string_of_thm rl))
   34.24 -            else ();
   34.25 -            Option.NONE);
   34.26 +  handle
   34.27 +    ElimBadPrem => (*reject: prems don't preserve conclusion*)
   34.28 +      (warning ("Ignoring weak elimination rule\n" ^ Display.string_of_thm_global thy rl);
   34.29 +        Option.NONE)
   34.30 +  | ElimBadConcl => (*ignore: conclusion is not just a variable*)
   34.31 +      (if !trace then
   34.32 +        (warning ("Ignoring ill-formed elimination rule:\n" ^
   34.33 +          "conclusion should be a variable\n" ^ Display.string_of_thm_global thy rl))
   34.34 +       else ();
   34.35 +       Option.NONE);
   34.36  
   34.37  
   34.38  (*** Conversion of Introduction Rules ***)
    35.1 --- a/src/Provers/classical.ML	Wed Jul 22 10:49:26 2009 +0200
    35.2 +++ b/src/Provers/classical.ML	Wed Jul 22 11:23:09 2009 +0200
    35.3 @@ -256,7 +256,7 @@
    35.4       xtra_netpair  = empty_netpair};
    35.5  
    35.6  fun print_cs (CS {safeIs, safeEs, hazIs, hazEs, swrappers, uwrappers, ...}) =
    35.7 -  let val pretty_thms = map Display.pretty_thm in
    35.8 +  let val pretty_thms = map Display.pretty_thm_without_context in
    35.9      [Pretty.big_list "safe introduction rules (intro!):" (pretty_thms safeIs),
   35.10        Pretty.big_list "introduction rules (intro):" (pretty_thms hazIs),
   35.11        Pretty.big_list "safe elimination rules (elim!):" (pretty_thms safeEs),
   35.12 @@ -313,14 +313,18 @@
   35.13  (*Warn if the rule is already present ELSEWHERE in the claset.  The addition
   35.14    is still allowed.*)
   35.15  fun warn_dup th (CS{safeIs, safeEs, hazIs, hazEs, ...}) =
   35.16 -       if mem_thm safeIs th then
   35.17 -         warning ("Rule already declared as safe introduction (intro!)\n" ^ Display.string_of_thm th)
   35.18 +  if mem_thm safeIs th then
   35.19 +    warning ("Rule already declared as safe introduction (intro!)\n" ^
   35.20 +      Display.string_of_thm_without_context th)
   35.21    else if mem_thm safeEs th then
   35.22 -         warning ("Rule already declared as safe elimination (elim!)\n" ^ Display.string_of_thm th)
   35.23 +    warning ("Rule already declared as safe elimination (elim!)\n" ^
   35.24 +      Display.string_of_thm_without_context th)
   35.25    else if mem_thm hazIs th then
   35.26 -         warning ("Rule already declared as introduction (intro)\n" ^ Display.string_of_thm th)
   35.27 +    warning ("Rule already declared as introduction (intro)\n" ^
   35.28 +      Display.string_of_thm_without_context th)
   35.29    else if mem_thm hazEs th then
   35.30 -         warning ("Rule already declared as elimination (elim)\n" ^ Display.string_of_thm th)
   35.31 +    warning ("Rule already declared as elimination (elim)\n" ^
   35.32 +      Display.string_of_thm_without_context th)
   35.33    else ();
   35.34  
   35.35  
   35.36 @@ -330,8 +334,8 @@
   35.37    (cs as CS {safeIs, safeEs, hazIs, hazEs, swrappers, uwrappers,
   35.38               safe0_netpair, safep_netpair, haz_netpair, dup_netpair, xtra_netpair}) =
   35.39    if mem_thm safeIs th then
   35.40 -         (warning ("Ignoring duplicate safe introduction (intro!)\n" ^ Display.string_of_thm th);
   35.41 -          cs)
   35.42 +    (warning ("Ignoring duplicate safe introduction (intro!)\n" ^
   35.43 +      Display.string_of_thm_without_context th); cs)
   35.44    else
   35.45    let val th' = flat_rule th
   35.46        val (safe0_rls, safep_rls) = (*0 subgoals vs 1 or more*)
   35.47 @@ -356,10 +360,10 @@
   35.48    (cs as CS {safeIs, safeEs, hazIs, hazEs, swrappers, uwrappers,
   35.49               safe0_netpair, safep_netpair, haz_netpair, dup_netpair, xtra_netpair}) =
   35.50    if mem_thm safeEs th then
   35.51 -         (warning ("Ignoring duplicate safe elimination (elim!)\n" ^ Display.string_of_thm th);
   35.52 -          cs)
   35.53 +    (warning ("Ignoring duplicate safe elimination (elim!)\n" ^
   35.54 +        Display.string_of_thm_without_context th); cs)
   35.55    else if has_fewer_prems 1 th then
   35.56 -    	error("Ill-formed elimination rule\n" ^ Display.string_of_thm th)
   35.57 +    	error ("Ill-formed elimination rule\n" ^ Display.string_of_thm_without_context th)
   35.58    else
   35.59    let
   35.60        val th' = classical_rule (flat_rule th)
   35.61 @@ -386,7 +390,7 @@
   35.62  
   35.63  fun make_elim th =
   35.64      if has_fewer_prems 1 th then
   35.65 -    	error("Ill-formed destruction rule\n" ^ Display.string_of_thm th)
   35.66 +    	  error ("Ill-formed destruction rule\n" ^ Display.string_of_thm_without_context th)
   35.67      else Tactic.make_elim th;
   35.68  
   35.69  fun cs addSDs ths = cs addSEs (map make_elim ths);
   35.70 @@ -398,8 +402,8 @@
   35.71    (cs as CS {safeIs, safeEs, hazIs, hazEs, swrappers, uwrappers,
   35.72               safe0_netpair, safep_netpair, haz_netpair, dup_netpair, xtra_netpair}) =
   35.73    if mem_thm hazIs th then
   35.74 -         (warning ("Ignoring duplicate introduction (intro)\n" ^ Display.string_of_thm th);
   35.75 -          cs)
   35.76 +    (warning ("Ignoring duplicate introduction (intro)\n" ^
   35.77 +        Display.string_of_thm_without_context th); cs)
   35.78    else
   35.79    let val th' = flat_rule th
   35.80        val nI = length hazIs + 1
   35.81 @@ -418,16 +422,16 @@
   35.82          xtra_netpair = insert' (the_default 1 w) (nI,nE) ([th], []) xtra_netpair}
   35.83    end
   35.84    handle THM("RSN: no unifiers",_,_) => (*from dup_intr*)
   35.85 -         error ("Ill-formed introduction rule\n" ^ Display.string_of_thm th);
   35.86 +    error ("Ill-formed introduction rule\n" ^ Display.string_of_thm_without_context th);
   35.87  
   35.88  fun addE w th
   35.89    (cs as CS {safeIs, safeEs, hazIs, hazEs, swrappers, uwrappers,
   35.90              safe0_netpair, safep_netpair, haz_netpair, dup_netpair, xtra_netpair}) =
   35.91    if mem_thm hazEs th then
   35.92 -         (warning ("Ignoring duplicate elimination (elim)\n" ^ Display.string_of_thm th);
   35.93 -          cs)
   35.94 +    (warning ("Ignoring duplicate elimination (elim)\n" ^
   35.95 +        Display.string_of_thm_without_context th); cs)
   35.96    else if has_fewer_prems 1 th then
   35.97 -    	error("Ill-formed elimination rule\n" ^ Display.string_of_thm th)
   35.98 +    	error("Ill-formed elimination rule\n" ^ Display.string_of_thm_without_context th)
   35.99    else
  35.100    let
  35.101        val th' = classical_rule (flat_rule th)
  35.102 @@ -519,7 +523,7 @@
  35.103      end
  35.104   else cs
  35.105   handle THM("RSN: no unifiers",_,_) => (*from dup_intr*)
  35.106 -        error ("Ill-formed introduction rule\n" ^ Display.string_of_thm th);
  35.107 +   error ("Ill-formed introduction rule\n" ^ Display.string_of_thm_without_context th);
  35.108  
  35.109  
  35.110  fun delE th
  35.111 @@ -548,7 +552,7 @@
  35.112        mem_thm hazIs th orelse mem_thm hazEs th orelse
  35.113        mem_thm safeEs th' orelse mem_thm hazEs th'
  35.114      then delSI th (delSE th (delI th (delE th (delSE th' (delE th' cs)))))
  35.115 -    else (warning ("Undeclared classical rule\n" ^ Display.string_of_thm th); cs)
  35.116 +    else (warning ("Undeclared classical rule\n" ^ Display.string_of_thm_without_context th); cs)
  35.117    end;
  35.118  
  35.119  fun cs delrules ths = fold delrule ths cs;
    36.1 --- a/src/Pure/Concurrent/future.ML	Wed Jul 22 10:49:26 2009 +0200
    36.2 +++ b/src/Pure/Concurrent/future.ML	Wed Jul 22 11:23:09 2009 +0200
    36.3 @@ -30,6 +30,7 @@
    36.4    type task = Task_Queue.task
    36.5    type group = Task_Queue.group
    36.6    val is_worker: unit -> bool
    36.7 +  val worker_group: unit -> Task_Queue.group option
    36.8    type 'a future
    36.9    val task_of: 'a future -> task
   36.10    val group_of: 'a future -> group
   36.11 @@ -40,7 +41,6 @@
   36.12    val fork_group: group -> (unit -> 'a) -> 'a future
   36.13    val fork_deps: 'b future list -> (unit -> 'a) -> 'a future
   36.14    val fork_pri: int -> (unit -> 'a) -> 'a future
   36.15 -  val fork_local: int -> (unit -> 'a) -> 'a future
   36.16    val join_results: 'a future list -> 'a Exn.result list
   36.17    val join_result: 'a future -> 'a Exn.result
   36.18    val join: 'a future -> 'a
   36.19 @@ -76,6 +76,7 @@
   36.20  end;
   36.21  
   36.22  val is_worker = is_some o thread_data;
   36.23 +val worker_group = Option.map #3 o thread_data;
   36.24  
   36.25  
   36.26  (* datatype future *)
   36.27 @@ -93,7 +94,7 @@
   36.28  
   36.29  fun value x = Future
   36.30   {task = Task_Queue.new_task 0,
   36.31 -  group = Task_Queue.new_group (),
   36.32 +  group = Task_Queue.new_group NONE,
   36.33    result = ref (SOME (Exn.Result x))};
   36.34  
   36.35  
   36.36 @@ -134,18 +135,43 @@
   36.37  
   36.38  (* worker activity *)
   36.39  
   36.40 -fun trace_active () =
   36.41 +fun count_active ws =
   36.42 +  fold (fn (_, active) => fn i => if active then i + 1 else i) ws 0;
   36.43 +
   36.44 +fun trace_active () = Multithreading.tracing 1 (fn () =>
   36.45    let
   36.46      val ws = ! workers;
   36.47      val m = string_of_int (length ws);
   36.48 -    val n = string_of_int (length (filter #2 ws));
   36.49 -  in Multithreading.tracing 2 (fn () => "SCHEDULE: " ^ m ^ " workers, " ^ n ^ " active") end;
   36.50 +    val n = string_of_int (count_active ws);
   36.51 +  in "SCHEDULE: " ^ m ^ " workers, " ^ n ^ " active" end);
   36.52  
   36.53  fun change_active active = (*requires SYNCHRONIZED*)
   36.54    change workers (AList.update Thread.equal (Thread.self (), active));
   36.55  
   36.56 +fun overloaded () =
   36.57 +  count_active (! workers) > Multithreading.max_threads_value ();
   36.58  
   36.59 -(* execute jobs *)
   36.60 +
   36.61 +(* execute future jobs *)
   36.62 +
   36.63 +fun future_job group (e: unit -> 'a) =
   36.64 +  let
   36.65 +    val result = ref (NONE: 'a Exn.result option);
   36.66 +    fun job ok =
   36.67 +      let
   36.68 +        val res =
   36.69 +          if ok then
   36.70 +            Exn.capture
   36.71 +              (Multithreading.with_attributes Multithreading.restricted_interrupts
   36.72 +                (fn _ => fn () => e ())) ()
   36.73 +          else Exn.Exn Exn.Interrupt;
   36.74 +        val _ = result := SOME res;
   36.75 +      in
   36.76 +        (case res of
   36.77 +          Exn.Exn exn => (Task_Queue.cancel_group group exn; false)
   36.78 +        | Exn.Result _ => true)
   36.79 +      end;
   36.80 +  in (result, job) end;
   36.81  
   36.82  fun do_cancel group = (*requires SYNCHRONIZED*)
   36.83    change canceled (insert Task_Queue.eq_group group);
   36.84 @@ -153,7 +179,7 @@
   36.85  fun execute name (task, group, jobs) =
   36.86    let
   36.87      val _ = trace_active ();
   36.88 -    val valid = Task_Queue.is_valid group;
   36.89 +    val valid = not (Task_Queue.is_canceled group);
   36.90      val ok = setmp_thread_data (name, task, group) (fn () =>
   36.91        fold (fn job => fn ok => job valid andalso ok) jobs true) ();
   36.92      val _ = SYNCHRONIZED "execute" (fn () =>
   36.93 @@ -176,13 +202,14 @@
   36.94       change workers (filter_out (fn (thread, _) => Thread.equal (thread, Thread.self ())));
   36.95       notify_all ();
   36.96       NONE)
   36.97 +  else if overloaded () then (worker_wait (); worker_next ())
   36.98    else
   36.99      (case change_result queue Task_Queue.dequeue of
  36.100        NONE => (worker_wait (); worker_next ())
  36.101      | some => some);
  36.102  
  36.103  fun worker_loop name =
  36.104 -  (case SYNCHRONIZED name worker_next of
  36.105 +  (case SYNCHRONIZED name (fn () => worker_next ()) of
  36.106      NONE => ()
  36.107    | SOME work => (execute name work; worker_loop name));
  36.108  
  36.109 @@ -204,26 +231,31 @@
  36.110        end);
  36.111  
  36.112      (*worker threads*)
  36.113 +    val ws = ! workers;
  36.114      val _ =
  36.115 -      (case List.partition (Thread.isActive o #1) (! workers) of
  36.116 -        (_, []) => ()
  36.117 -      | (active, inactive) =>
  36.118 -          (workers := active; Multithreading.tracing 0 (fn () =>
  36.119 -            "SCHEDULE: disposed " ^ string_of_int (length inactive) ^ " dead worker threads")));
  36.120 +      if forall (Thread.isActive o #1) ws then ()
  36.121 +      else
  36.122 +        (case List.partition (Thread.isActive o #1) ws of
  36.123 +          (_, []) => ()
  36.124 +        | (active, inactive) =>
  36.125 +            (workers := active; Multithreading.tracing 0 (fn () =>
  36.126 +              "SCHEDULE: disposed " ^ string_of_int (length inactive) ^ " dead worker threads")));
  36.127      val _ = trace_active ();
  36.128  
  36.129      val m = if ! do_shutdown then 0 else Multithreading.max_threads_value ();
  36.130 -    val l = length (! workers);
  36.131 -    val _ = excessive := l - m;
  36.132 +    val mm = (m * 3) div 2;
  36.133 +    val l = length ws;
  36.134 +    val _ = excessive := l - mm;
  36.135      val _ =
  36.136 -      if m > l then funpow (m - l) (fn () => worker_start ("worker " ^ string_of_int (inc next))) ()
  36.137 +      if mm > l then
  36.138 +        funpow (mm - l) (fn () => worker_start ("worker " ^ string_of_int (inc next))) ()
  36.139        else ();
  36.140  
  36.141      (*canceled groups*)
  36.142 -    val _ =  change canceled (filter_out (Task_Queue.cancel (! queue)));
  36.143 +    val _ = change canceled (filter_out (Task_Queue.cancel (! queue)));
  36.144  
  36.145      (*shutdown*)
  36.146 -    val continue = not (! do_shutdown andalso null (! workers));
  36.147 +    val continue = not (! do_shutdown andalso null ws);
  36.148      val _ = if continue then () else scheduler := NONE;
  36.149  
  36.150      val _ = notify_all ();
  36.151 @@ -233,7 +265,7 @@
  36.152    in continue end;
  36.153  
  36.154  fun scheduler_loop () =
  36.155 -  while SYNCHRONIZED "scheduler" scheduler_next do ();
  36.156 +  while SYNCHRONIZED "scheduler" (fn () => scheduler_next ()) do ();
  36.157  
  36.158  fun scheduler_active () = (*requires SYNCHRONIZED*)
  36.159    (case ! scheduler of NONE => false | SOME thread => Thread.isActive thread);
  36.160 @@ -248,32 +280,16 @@
  36.161  
  36.162  (** futures **)
  36.163  
  36.164 -(* future job: fill result *)
  36.165 -
  36.166 -fun future_job group (e: unit -> 'a) =
  36.167 -  let
  36.168 -    val result = ref (NONE: 'a Exn.result option);
  36.169 -    val job = Multithreading.with_attributes Multithreading.restricted_interrupts
  36.170 -      (fn _ => fn ok =>
  36.171 -        let
  36.172 -          val res = if ok then Exn.capture e () else Exn.Exn Exn.Interrupt;
  36.173 -          val _ = result := SOME res;
  36.174 -          val res_ok =
  36.175 -            (case res of
  36.176 -              Exn.Result _ => true
  36.177 -            | Exn.Exn Exn.Interrupt => (Task_Queue.invalidate_group group; true)
  36.178 -            | _ => false);
  36.179 -        in res_ok end);
  36.180 -  in (result, job) end;
  36.181 -
  36.182 -
  36.183  (* fork *)
  36.184  
  36.185  fun fork_future opt_group deps pri e =
  36.186    let
  36.187      val _ = scheduler_check "future check";
  36.188  
  36.189 -    val group = (case opt_group of SOME group => group | NONE => Task_Queue.new_group ());
  36.190 +    val group =
  36.191 +      (case opt_group of
  36.192 +        SOME group => group
  36.193 +      | NONE => Task_Queue.new_group (worker_group ()));
  36.194      val (result, job) = future_job group e;
  36.195      val task = SYNCHRONIZED "future" (fn () =>
  36.196        change_result queue (Task_Queue.enqueue group deps pri job) before notify_all ());
  36.197 @@ -283,17 +299,25 @@
  36.198  fun fork_group group e = fork_future (SOME group) [] 0 e;
  36.199  fun fork_deps deps e = fork_future NONE (map task_of deps) 0 e;
  36.200  fun fork_pri pri e = fork_future NONE [] pri e;
  36.201 -fun fork_local pri e = fork_future (Option.map #3 (thread_data ())) [] pri e;
  36.202  
  36.203  
  36.204  (* join *)
  36.205  
  36.206  local
  36.207  
  36.208 -fun get_result x = the_default (Exn.Exn (SYS_ERROR "unfinished future")) (peek x);
  36.209 +fun get_result x =
  36.210 +  (case peek x of
  36.211 +    NONE => Exn.Exn (SYS_ERROR "unfinished future")
  36.212 +  | SOME (Exn.Exn Exn.Interrupt) =>
  36.213 +      Exn.Exn (Exn.EXCEPTIONS (Exn.flatten_list (Task_Queue.group_status (group_of x))))
  36.214 +  | SOME res => res);
  36.215 +
  36.216 +fun join_next deps = (*requires SYNCHRONIZED*)
  36.217 +  if overloaded () then (worker_wait (); join_next deps)
  36.218 +  else change_result queue (Task_Queue.dequeue_towards deps);
  36.219  
  36.220  fun join_deps deps =
  36.221 -  (case SYNCHRONIZED "join" (fn () => change_result queue (Task_Queue.dequeue_towards deps)) of
  36.222 +  (case SYNCHRONIZED "join" (fn () => join_next deps) of
  36.223      NONE => ()
  36.224    | SOME (work, deps') => (execute "join" work; join_deps deps'));
  36.225  
  36.226 @@ -308,12 +332,12 @@
  36.227          error "Cannot join future values within critical section";
  36.228  
  36.229        val worker = is_worker ();
  36.230 +      val _ = if worker then join_deps (map task_of xs) else ();
  36.231 +
  36.232        fun join_wait x =
  36.233          if SYNCHRONIZED "join_wait" (fn () =>
  36.234            is_finished x orelse (if worker then worker_wait () else wait (); false))
  36.235          then () else join_wait x;
  36.236 -
  36.237 -      val _ = if worker then join_deps (map task_of xs) else ();
  36.238        val _ = List.app join_wait xs;
  36.239  
  36.240      in map get_result xs end) ();
  36.241 @@ -331,7 +355,7 @@
  36.242      val _ = scheduler_check "map_future check";
  36.243  
  36.244      val task = task_of x;
  36.245 -    val group = Task_Queue.new_group ();
  36.246 +    val group = Task_Queue.new_group (SOME (group_of x));
  36.247      val (result, job) = future_job group (fn () => f (join x));
  36.248  
  36.249      val extended = SYNCHRONIZED "map_future" (fn () =>
  36.250 @@ -340,7 +364,7 @@
  36.251        | NONE => false));
  36.252    in
  36.253      if extended then Future {task = task, group = group, result = result}
  36.254 -    else fork_future NONE [task] (Task_Queue.pri_of_task task) (fn () => f (join x))
  36.255 +    else fork_future (SOME group) [task] (Task_Queue.pri_of_task task) (fn () => f (join x))
  36.256    end;
  36.257  
  36.258  
    37.1 --- a/src/Pure/Concurrent/par_list.ML	Wed Jul 22 10:49:26 2009 +0200
    37.2 +++ b/src/Pure/Concurrent/par_list.ML	Wed Jul 22 11:23:09 2009 +0200
    37.3 @@ -28,11 +28,8 @@
    37.4  
    37.5  fun raw_map f xs =
    37.6    if Future.enabled () then
    37.7 -    let
    37.8 -      val group = Task_Queue.new_group ();
    37.9 -      val futures = map (fn x => Future.fork_group group (fn () => f x)) xs;
   37.10 -      val _ = List.app (ignore o Future.join_result) futures;
   37.11 -    in Future.join_results futures end
   37.12 +    let val group = Task_Queue.new_group (Future.worker_group ())
   37.13 +    in Future.join_results (map (fn x => Future.fork_group group (fn () => f x)) xs) end
   37.14    else map (Exn.capture f) xs;
   37.15  
   37.16  fun map f xs = Exn.release_first (raw_map f xs);
    38.1 --- a/src/Pure/Concurrent/task_queue.ML	Wed Jul 22 10:49:26 2009 +0200
    38.2 +++ b/src/Pure/Concurrent/task_queue.ML	Wed Jul 22 11:23:09 2009 +0200
    38.3 @@ -13,9 +13,8 @@
    38.4    type group
    38.5    val group_id: group -> int
    38.6    val eq_group: group * group -> bool
    38.7 -  val new_group: unit -> group
    38.8 -  val is_valid: group -> bool
    38.9 -  val invalidate_group: group -> unit
   38.10 +  val new_group: group option -> group
   38.11 +  val group_status: group -> exn list
   38.12    val str_of_group: group -> string
   38.13    type queue
   38.14    val empty: queue
   38.15 @@ -28,6 +27,8 @@
   38.16      (((task * group * (bool -> bool) list) * task list) option * queue)
   38.17    val interrupt: queue -> task -> unit
   38.18    val interrupt_external: queue -> string -> unit
   38.19 +  val is_canceled: group -> bool
   38.20 +  val cancel_group: group -> exn -> unit
   38.21    val cancel: queue -> group -> bool
   38.22    val cancel_all: queue -> group list
   38.23    val finish: task -> queue -> queue
   38.24 @@ -48,20 +49,37 @@
   38.25  structure Task_Graph = Graph(type key = task val ord = task_ord);
   38.26  
   38.27  
   38.28 -(* groups *)
   38.29 +(* nested groups *)
   38.30 +
   38.31 +datatype group = Group of
   38.32 + {parent: group option,
   38.33 +  id: serial,
   38.34 +  status: exn list ref};
   38.35  
   38.36 -datatype group = Group of serial * bool ref;
   38.37 +fun make_group (parent, id, status) = Group {parent = parent, id = id, status = status};
   38.38  
   38.39 -fun group_id (Group (gid, _)) = gid;
   38.40 -fun eq_group (Group (gid1, _), Group (gid2, _)) = gid1 = gid2;
   38.41 +fun new_group parent = make_group (parent, serial (), ref []);
   38.42 +
   38.43 +fun group_id (Group {id, ...}) = id;
   38.44 +fun eq_group (group1, group2) = group_id group1 = group_id group2;
   38.45  
   38.46 -fun new_group () = Group (serial (), ref true);
   38.47 +fun group_ancestry (Group {parent, id, ...}) =
   38.48 +  id :: (case parent of NONE => [] | SOME group => group_ancestry group);
   38.49 +
   38.50 +
   38.51 +fun cancel_group (Group {status, ...}) exn = CRITICAL (fn () =>
   38.52 +  (case exn of
   38.53 +    Exn.Interrupt => if null (! status) then status := [exn] else ()
   38.54 +  | _ => change status (cons exn)));
   38.55  
   38.56 -fun is_valid (Group (_, ref ok)) = ok;
   38.57 -fun invalidate_group (Group (_, ok)) = ok := false;
   38.58 +fun group_status (Group {parent, status, ...}) = (*non-critical*)
   38.59 +  ! status @ (case parent of NONE => [] | SOME group => group_status group);
   38.60  
   38.61 -fun str_of_group (Group (i, ref ok)) =
   38.62 -  if ok then string_of_int i else enclose "(" ")" (string_of_int i);
   38.63 +fun is_canceled (Group {parent, status, ...}) = (*non-critical*)
   38.64 +  not (null (! status)) orelse (case parent of NONE => false | SOME group => is_canceled group);
   38.65 +
   38.66 +fun str_of_group group =
   38.67 +  (is_canceled group ? enclose "(" ")") (string_of_int (group_id group));
   38.68  
   38.69  
   38.70  (* jobs *)
   38.71 @@ -95,7 +113,7 @@
   38.72  fun is_empty (Queue {jobs, ...}) = Task_Graph.is_empty jobs;
   38.73  
   38.74  
   38.75 -(* status *)
   38.76 +(* queue status *)
   38.77  
   38.78  fun status (Queue {jobs, ...}) =
   38.79    let
   38.80 @@ -108,14 +126,38 @@
   38.81    in {ready = x, pending = y, running = z} end;
   38.82  
   38.83  
   38.84 +(* cancel -- peers and sub-groups *)
   38.85 +
   38.86 +fun cancel (Queue {groups, jobs, ...}) group =
   38.87 +  let
   38.88 +    val _ = cancel_group group Exn.Interrupt;
   38.89 +    val tasks = Inttab.lookup_list groups (group_id group);
   38.90 +    val running =
   38.91 +      fold (get_job jobs #> (fn Running t => insert Thread.equal t | _ => I)) tasks [];
   38.92 +    val _ = List.app SimpleThread.interrupt running;
   38.93 +  in null running end;
   38.94 +
   38.95 +fun cancel_all (Queue {jobs, ...}) =
   38.96 +  let
   38.97 +    fun cancel_job (group, job) (groups, running) =
   38.98 +      (cancel_group group Exn.Interrupt;
   38.99 +        (case job of Running t => (insert eq_group group groups, insert Thread.equal t running)
  38.100 +        | _ => (groups, running)));
  38.101 +    val (groups, running) = Task_Graph.fold (cancel_job o #1 o #2) jobs ([], []);
  38.102 +    val _ = List.app SimpleThread.interrupt running;
  38.103 +  in groups end;
  38.104 +
  38.105 +
  38.106  (* enqueue *)
  38.107  
  38.108 -fun enqueue (group as Group (gid, _)) deps pri job (Queue {groups, jobs, cache}) =
  38.109 +fun enqueue group deps pri job (Queue {groups, jobs, cache}) =
  38.110    let
  38.111      val task = new_task pri;
  38.112 -    val groups' = Inttab.cons_list (gid, task) groups;
  38.113 +    val groups' = groups
  38.114 +      |> fold (fn gid => Inttab.cons_list (gid, task)) (group_ancestry group);
  38.115      val jobs' = jobs
  38.116 -      |> Task_Graph.new_node (task, (group, Job [job])) |> fold (add_job task) deps;
  38.117 +      |> Task_Graph.new_node (task, (group, Job [job]))
  38.118 +      |> fold (add_job task) deps;
  38.119      val cache' =
  38.120        (case cache of
  38.121          Result last =>
  38.122 @@ -159,25 +201,33 @@
  38.123      fun ready task =
  38.124        (case Task_Graph.get_node jobs task of
  38.125          (group, Job list) =>
  38.126 -          if null (Task_Graph.imm_preds jobs task) then SOME (task, group, rev list)
  38.127 +          if null (Task_Graph.imm_preds jobs task)
  38.128 +          then SOME (task, group, rev list)
  38.129            else NONE
  38.130        | _ => NONE);
  38.131 +
  38.132      val tasks = filter (can (Task_Graph.get_node jobs)) deps;
  38.133 +    fun result (res as (task, _, _)) =
  38.134 +      let
  38.135 +        val jobs' = set_job task (Running (Thread.self ())) jobs;
  38.136 +        val cache' = Unknown;
  38.137 +      in (SOME (res, tasks), make_queue groups jobs' cache') end;
  38.138    in
  38.139 -    (case get_first ready (Task_Graph.all_preds jobs tasks) of
  38.140 -      NONE => (NONE, queue)
  38.141 -    | SOME (result as (task, _, _)) =>
  38.142 -        let
  38.143 -          val jobs' = set_job task (Running (Thread.self ())) jobs;
  38.144 -          val cache' = Unknown;
  38.145 -        in (SOME (result, tasks), make_queue groups jobs' cache') end)
  38.146 +    (case get_first ready tasks of
  38.147 +      SOME res => result res
  38.148 +    | NONE =>
  38.149 +        (case get_first ready (Task_Graph.all_preds jobs tasks) of
  38.150 +          SOME res => result res
  38.151 +        | NONE => (NONE, queue)))
  38.152    end;
  38.153  
  38.154  
  38.155  (* sporadic interrupts *)
  38.156  
  38.157  fun interrupt (Queue {jobs, ...}) task =
  38.158 -  (case try (get_job jobs) task of SOME (Running thread) => SimpleThread.interrupt thread | _ => ());
  38.159 +  (case try (get_job jobs) task of
  38.160 +    SOME (Running thread) => SimpleThread.interrupt thread
  38.161 +  | _ => ());
  38.162  
  38.163  fun interrupt_external (queue as Queue {jobs, ...}) str =
  38.164    (case Int.fromString str of
  38.165 @@ -190,28 +240,11 @@
  38.166  
  38.167  (* termination *)
  38.168  
  38.169 -fun cancel (Queue {groups, jobs, ...}) (group as Group (gid, _)) =
  38.170 -  let
  38.171 -    val _ = invalidate_group group;
  38.172 -    val tasks = Inttab.lookup_list groups gid;
  38.173 -    val running = fold (get_job jobs #> (fn Running t => insert Thread.equal t | _ => I)) tasks [];
  38.174 -    val _ = List.app SimpleThread.interrupt running;
  38.175 -  in null running end;
  38.176 -
  38.177 -fun cancel_all (Queue {jobs, ...}) =
  38.178 -  let
  38.179 -    fun cancel_job (group, job) (groups, running) =
  38.180 -      (invalidate_group group;
  38.181 -        (case job of Running t => (insert eq_group group groups, insert Thread.equal t running)
  38.182 -        | _ => (groups, running)));
  38.183 -    val (groups, running) = Task_Graph.fold (cancel_job o #1 o #2) jobs ([], []);
  38.184 -    val _ = List.app SimpleThread.interrupt running;
  38.185 -  in groups end;
  38.186 -
  38.187  fun finish task (Queue {groups, jobs, cache}) =
  38.188    let
  38.189 -    val Group (gid, _) = get_group jobs task;
  38.190 -    val groups' = Inttab.remove_list (op =) (gid, task) groups;
  38.191 +    val group = get_group jobs task;
  38.192 +    val groups' = groups
  38.193 +      |> fold (fn gid => Inttab.remove_list (op =) (gid, task)) (group_ancestry group);
  38.194      val jobs' = Task_Graph.del_node task jobs;
  38.195      val cache' =
  38.196        if null (Task_Graph.imm_succs jobs task) then cache
    39.1 --- a/src/Pure/IsaMakefile	Wed Jul 22 10:49:26 2009 +0200
    39.2 +++ b/src/Pure/IsaMakefile	Wed Jul 22 11:23:09 2009 +0200
    39.3 @@ -90,13 +90,13 @@
    39.4    Tools/find_theorems.ML Tools/named_thms.ML Tools/xml_syntax.ML	\
    39.5    assumption.ML axclass.ML codegen.ML config.ML conjunction.ML		\
    39.6    consts.ML context.ML context_position.ML conv.ML defs.ML display.ML	\
    39.7 -  drule.ML envir.ML facts.ML goal.ML interpretation.ML item_net.ML	\
    39.8 -  library.ML logic.ML meta_simplifier.ML more_thm.ML morphism.ML	\
    39.9 -  name.ML net.ML old_goals.ML old_term.ML pattern.ML primitive_defs.ML	\
   39.10 -  proofterm.ML pure_setup.ML pure_thy.ML search.ML sign.ML		\
   39.11 -  simplifier.ML sorts.ML subgoal.ML tactic.ML tctical.ML term.ML	\
   39.12 -  term_ord.ML term_subst.ML theory.ML thm.ML type.ML type_infer.ML	\
   39.13 -  unify.ML variable.ML
   39.14 +  display_goal.ML drule.ML envir.ML facts.ML goal.ML interpretation.ML	\
   39.15 +  item_net.ML library.ML logic.ML meta_simplifier.ML more_thm.ML	\
   39.16 +  morphism.ML name.ML net.ML old_goals.ML old_term.ML pattern.ML	\
   39.17 +  primitive_defs.ML proofterm.ML pure_setup.ML pure_thy.ML search.ML	\
   39.18 +  sign.ML simplifier.ML sorts.ML subgoal.ML tactic.ML tctical.ML	\
   39.19 +  term.ML term_ord.ML term_subst.ML theory.ML thm.ML type.ML		\
   39.20 +  type_infer.ML unify.ML variable.ML
   39.21  	@./mk
   39.22  
   39.23  
    40.1 --- a/src/Pure/Isar/args.ML	Wed Jul 22 10:49:26 2009 +0200
    40.2 +++ b/src/Pure/Isar/args.ML	Wed Jul 22 11:23:09 2009 +0200
    40.3 @@ -88,7 +88,7 @@
    40.4  
    40.5  fun pretty_src ctxt src =
    40.6    let
    40.7 -    val prt_thm = Pretty.backquote o ProofContext.pretty_thm ctxt;
    40.8 +    val prt_thm = Pretty.backquote o Display.pretty_thm ctxt;
    40.9      fun prt arg =
   40.10        (case T.get_value arg of
   40.11          SOME (T.Text s) => Pretty.str (quote s)
    41.1 --- a/src/Pure/Isar/calculation.ML	Wed Jul 22 10:49:26 2009 +0200
    41.2 +++ b/src/Pure/Isar/calculation.ML	Wed Jul 22 11:23:09 2009 +0200
    41.3 @@ -40,8 +40,8 @@
    41.4  fun print_rules ctxt =
    41.5    let val ((trans, sym), _) = CalculationData.get (Context.Proof ctxt) in
    41.6      [Pretty.big_list "transitivity rules:"
    41.7 -        (map (ProofContext.pretty_thm ctxt) (Item_Net.content trans)),
    41.8 -      Pretty.big_list "symmetry rules:" (map (ProofContext.pretty_thm ctxt) sym)]
    41.9 +        (map (Display.pretty_thm ctxt) (Item_Net.content trans)),
   41.10 +      Pretty.big_list "symmetry rules:" (map (Display.pretty_thm ctxt) sym)]
   41.11      |> Pretty.chunks |> Pretty.writeln
   41.12    end;
   41.13  
    42.1 --- a/src/Pure/Isar/code.ML	Wed Jul 22 10:49:26 2009 +0200
    42.2 +++ b/src/Pure/Isar/code.ML	Wed Jul 22 11:23:09 2009 +0200
    42.3 @@ -243,7 +243,7 @@
    42.4    (*default flag, theorems with proper flag (perhaps lazy)*)
    42.5  
    42.6  fun pretty_lthms ctxt r = case Lazy.peek r
    42.7 - of SOME thms => map (ProofContext.pretty_thm ctxt o fst) (Exn.release thms)
    42.8 + of SOME thms => map (Display.pretty_thm ctxt o fst) (Exn.release thms)
    42.9    | NONE => [Pretty.str "[...]"];
   42.10  
   42.11  fun certificate thy f r =
   42.12 @@ -263,7 +263,8 @@
   42.13        Pattern.matchess thy (args, (map incr_idx o curry Library.take (length args)) args');
   42.14      fun drop (thm', proper') = if (proper orelse not proper')
   42.15        andalso matches_args (args_of thm') then 
   42.16 -        (warning ("Code generator: dropping redundant code equation\n" ^ Display.string_of_thm thm'); true)
   42.17 +        (warning ("Code generator: dropping redundant code equation\n" ^
   42.18 +            Display.string_of_thm_global thy thm'); true)
   42.19        else false;
   42.20    in (thm, proper) :: filter_out drop thms end;
   42.21  
   42.22 @@ -567,16 +568,16 @@
   42.23  fun gen_assert_eqn thy is_constr_pat (thm, proper) =
   42.24    let
   42.25      val (lhs, rhs) = (Logic.dest_equals o Thm.plain_prop_of) thm
   42.26 -      handle TERM _ => bad_thm ("Not an equation: " ^ Display.string_of_thm thm)
   42.27 -           | THM _ => bad_thm ("Not an equation: " ^ Display.string_of_thm thm);
   42.28 +      handle TERM _ => bad_thm ("Not an equation: " ^ Display.string_of_thm_global thy thm)
   42.29 +           | THM _ => bad_thm ("Not an equation: " ^ Display.string_of_thm_global thy thm);
   42.30      fun vars_of t = fold_aterms (fn Var (v, _) => insert (op =) v
   42.31        | Free _ => bad_thm ("Illegal free variable in equation\n"
   42.32 -          ^ Display.string_of_thm thm)
   42.33 +          ^ Display.string_of_thm_global thy thm)
   42.34        | _ => I) t [];
   42.35      fun tvars_of t = fold_term_types (fn _ =>
   42.36        fold_atyps (fn TVar (v, _) => insert (op =) v
   42.37          | TFree _ => bad_thm 
   42.38 -      ("Illegal free type variable in equation\n" ^ Display.string_of_thm thm))) t [];
   42.39 +      ("Illegal free type variable in equation\n" ^ Display.string_of_thm_global thy thm))) t [];
   42.40      val lhs_vs = vars_of lhs;
   42.41      val rhs_vs = vars_of rhs;
   42.42      val lhs_tvs = tvars_of lhs;
   42.43 @@ -584,47 +585,48 @@
   42.44      val _ = if null (subtract (op =) lhs_vs rhs_vs)
   42.45        then ()
   42.46        else bad_thm ("Free variables on right hand side of equation\n"
   42.47 -        ^ Display.string_of_thm thm);
   42.48 +        ^ Display.string_of_thm_global thy thm);
   42.49      val _ = if null (subtract (op =) lhs_tvs rhs_tvs)
   42.50        then ()
   42.51        else bad_thm ("Free type variables on right hand side of equation\n"
   42.52 -        ^ Display.string_of_thm thm)    val (head, args) = (strip_comb o fst o Logic.dest_equals o Thm.plain_prop_of) thm;
   42.53 +        ^ Display.string_of_thm_global thy thm)
   42.54 +    val (head, args) = (strip_comb o fst o Logic.dest_equals o Thm.plain_prop_of) thm;
   42.55      val (c, ty) = case head
   42.56       of Const (c_ty as (_, ty)) => (AxClass.unoverload_const thy c_ty, ty)
   42.57 -      | _ => bad_thm ("Equation not headed by constant\n" ^ Display.string_of_thm thm);
   42.58 +      | _ => bad_thm ("Equation not headed by constant\n" ^ Display.string_of_thm_global thy thm);
   42.59      fun check _ (Abs _) = bad_thm
   42.60            ("Abstraction on left hand side of equation\n"
   42.61 -            ^ Display.string_of_thm thm)
   42.62 +            ^ Display.string_of_thm_global thy thm)
   42.63        | check 0 (Var _) = ()
   42.64        | check _ (Var _) = bad_thm
   42.65            ("Variable with application on left hand side of equation\n"
   42.66 -            ^ Display.string_of_thm thm)
   42.67 +            ^ Display.string_of_thm_global thy thm)
   42.68        | check n (t1 $ t2) = (check (n+1) t1; check 0 t2)
   42.69        | check n (Const (c_ty as (c, ty))) = if n = (length o fst o strip_type) ty
   42.70            then if not proper orelse is_constr_pat (AxClass.unoverload_const thy c_ty)
   42.71              then ()
   42.72              else bad_thm (quote c ^ " is not a constructor, on left hand side of equation\n"
   42.73 -              ^ Display.string_of_thm thm)
   42.74 +              ^ Display.string_of_thm_global thy thm)
   42.75            else bad_thm
   42.76              ("Partially applied constant " ^ quote c ^ " on left hand side of equation\n"
   42.77 -               ^ Display.string_of_thm thm);
   42.78 +               ^ Display.string_of_thm_global thy thm);
   42.79      val _ = map (check 0) args;
   42.80      val _ = if not proper orelse is_linear thm then ()
   42.81        else bad_thm ("Duplicate variables on left hand side of equation\n"
   42.82 -        ^ Display.string_of_thm thm);
   42.83 +        ^ Display.string_of_thm_global thy thm);
   42.84      val _ = if (is_none o AxClass.class_of_param thy) c
   42.85        then ()
   42.86        else bad_thm ("Polymorphic constant as head in equation\n"
   42.87 -        ^ Display.string_of_thm thm)
   42.88 +        ^ Display.string_of_thm_global thy thm)
   42.89      val _ = if not (is_constr thy c)
   42.90        then ()
   42.91        else bad_thm ("Constructor as head in equation\n"
   42.92 -        ^ Display.string_of_thm thm)
   42.93 +        ^ Display.string_of_thm_global thy thm)
   42.94      val ty_decl = Sign.the_const_type thy c;
   42.95      val _ = if Sign.typ_equiv thy (Type.strip_sorts ty_decl, Type.strip_sorts ty)
   42.96        then () else bad_thm ("Type\n" ^ string_of_typ thy ty
   42.97             ^ "\nof equation\n"
   42.98 -           ^ Display.string_of_thm thm
   42.99 +           ^ Display.string_of_thm_global thy thm
  42.100             ^ "\nis incompatible with declared function type\n"
  42.101             ^ string_of_typ thy ty_decl)
  42.102    in (thm, proper) end;
  42.103 @@ -657,7 +659,7 @@
  42.104    let
  42.105      fun cert (eqn as (thm, _)) = if c = const_eqn thy thm
  42.106        then eqn else error ("Wrong head of code equation,\nexpected constant "
  42.107 -        ^ string_of_const thy c ^ "\n" ^ Display.string_of_thm thm)
  42.108 +        ^ string_of_const thy c ^ "\n" ^ Display.string_of_thm_global thy thm)
  42.109    in map (cert o assert_eqn thy) eqns end;
  42.110  
  42.111  fun common_typ_eqns thy [] = []
  42.112 @@ -674,7 +676,7 @@
  42.113          fun unify ty env = Sign.typ_unify thy (ty1, ty) env
  42.114            handle Type.TUNIFY =>
  42.115              error ("Type unificaton failed, while unifying code equations\n"
  42.116 -            ^ (cat_lines o map Display.string_of_thm) thms
  42.117 +            ^ (cat_lines o map (Display.string_of_thm_global thy)) thms
  42.118              ^ "\nwith types\n"
  42.119              ^ (cat_lines o map (string_of_typ thy)) (ty1 :: tys));
  42.120          val (env, _) = fold unify tys (Vartab.empty, maxidx)
  42.121 @@ -796,17 +798,17 @@
  42.122    let
  42.123      val (ofclass, eqn) = case try Logic.dest_equals (Thm.prop_of thm)
  42.124       of SOME ofclass_eq => ofclass_eq
  42.125 -      | _ => error ("Bad certificate: " ^ Display.string_of_thm thm);
  42.126 +      | _ => error ("Bad certificate: " ^ Display.string_of_thm_global thy thm);
  42.127      val (T, class) = case try Logic.dest_of_class ofclass
  42.128       of SOME T_class => T_class
  42.129 -      | _ => error ("Bad certificate: " ^ Display.string_of_thm thm);
  42.130 +      | _ => error ("Bad certificate: " ^ Display.string_of_thm_global thy thm);
  42.131      val tvar = case try Term.dest_TVar T
  42.132       of SOME (tvar as (_, sort)) => if null (filter (can (AxClass.get_info thy)) sort)
  42.133            then tvar
  42.134 -          else error ("Bad sort: " ^ Display.string_of_thm thm)
  42.135 -      | _ => error ("Bad type: " ^ Display.string_of_thm thm);
  42.136 +          else error ("Bad sort: " ^ Display.string_of_thm_global thy thm)
  42.137 +      | _ => error ("Bad type: " ^ Display.string_of_thm_global thy thm);
  42.138      val _ = if Term.add_tvars eqn [] = [tvar] then ()
  42.139 -      else error ("Inconsistent type: " ^ Display.string_of_thm thm);
  42.140 +      else error ("Inconsistent type: " ^ Display.string_of_thm_global thy thm);
  42.141      val lhs_rhs = case try Logic.dest_equals eqn
  42.142       of SOME lhs_rhs => lhs_rhs
  42.143        | _ => error ("Not an equation: " ^ Syntax.string_of_term_global thy eqn);
  42.144 @@ -815,7 +817,7 @@
  42.145        | _ => error ("Not an equation with two constants: "
  42.146            ^ Syntax.string_of_term_global thy eqn);
  42.147      val _ = if the_list (AxClass.class_of_param thy (snd c_c')) = [class] then ()
  42.148 -      else error ("Inconsistent class: " ^ Display.string_of_thm thm);
  42.149 +      else error ("Inconsistent class: " ^ Display.string_of_thm_global thy thm);
  42.150    in thy |>
  42.151      (map_exec_purge NONE o map_aliasses) (fn (alias, classes) =>
  42.152        ((c_c', thm) :: alias, insert (op =) class classes))
    43.1 --- a/src/Pure/Isar/context_rules.ML	Wed Jul 22 10:49:26 2009 +0200
    43.2 +++ b/src/Pure/Isar/context_rules.ML	Wed Jul 22 11:23:09 2009 +0200
    43.3 @@ -116,7 +116,7 @@
    43.4      fun prt_kind (i, b) =
    43.5        Pretty.big_list ((the o AList.lookup (op =) kind_names) (i, b) ^ ":")
    43.6          (map_filter (fn (_, (k, th)) =>
    43.7 -            if k = (i, b) then SOME (ProofContext.pretty_thm ctxt th) else NONE)
    43.8 +            if k = (i, b) then SOME (Display.pretty_thm ctxt th) else NONE)
    43.9            (sort (int_ord o pairself fst) rules));
   43.10    in Pretty.writeln (Pretty.chunks (map prt_kind rule_kinds)) end;
   43.11  
    44.1 --- a/src/Pure/Isar/element.ML	Wed Jul 22 10:49:26 2009 +0200
    44.2 +++ b/src/Pure/Isar/element.ML	Wed Jul 22 11:23:09 2009 +0200
    44.3 @@ -163,7 +163,7 @@
    44.4    let
    44.5      val prt_typ = Pretty.quote o Syntax.pretty_typ ctxt;
    44.6      val prt_term = Pretty.quote o Syntax.pretty_term ctxt;
    44.7 -    val prt_thm = Pretty.backquote o ProofContext.pretty_thm ctxt;
    44.8 +    val prt_thm = Pretty.backquote o Display.pretty_thm ctxt;
    44.9      val prt_name_atts = pretty_name_atts ctxt;
   44.10  
   44.11      fun prt_mixfix NoSyn = []
    45.1 --- a/src/Pure/Isar/isar_cmd.ML	Wed Jul 22 10:49:26 2009 +0200
    45.2 +++ b/src/Pure/Isar/isar_cmd.ML	Wed Jul 22 11:23:09 2009 +0200
    45.3 @@ -442,8 +442,7 @@
    45.4    |> Pretty.chunks2 |> Pretty.string_of;
    45.5  
    45.6  fun string_of_thms state args =
    45.7 -  Pretty.string_of (ProofContext.pretty_thms (Proof.context_of state)
    45.8 -    (Proof.get_thmss state args));
    45.9 +  Pretty.string_of (Display.pretty_thms (Proof.context_of state) (Proof.get_thmss state args));
   45.10  
   45.11  fun string_of_prfs full state arg =
   45.12    Pretty.string_of (case arg of
    46.1 --- a/src/Pure/Isar/local_defs.ML	Wed Jul 22 10:49:26 2009 +0200
    46.2 +++ b/src/Pure/Isar/local_defs.ML	Wed Jul 22 11:23:09 2009 +0200
    46.3 @@ -196,7 +196,7 @@
    46.4  
    46.5  fun print_rules ctxt =
    46.6    Pretty.writeln (Pretty.big_list "definitional transformations:"
    46.7 -    (map (ProofContext.pretty_thm ctxt) (Rules.get (Context.Proof ctxt))));
    46.8 +    (map (Display.pretty_thm ctxt) (Rules.get (Context.Proof ctxt))));
    46.9  
   46.10  val defn_add = Thm.declaration_attribute (Rules.map o Thm.add_thm);
   46.11  val defn_del = Thm.declaration_attribute (Rules.map o Thm.del_thm);
    47.1 --- a/src/Pure/Isar/method.ML	Wed Jul 22 10:49:26 2009 +0200
    47.2 +++ b/src/Pure/Isar/method.ML	Wed Jul 22 11:23:09 2009 +0200
    47.3 @@ -220,7 +220,7 @@
    47.4  
    47.5  fun trace ctxt rules =
    47.6    if ! trace_rules andalso not (null rules) then
    47.7 -    Pretty.big_list "rules:" (map (ProofContext.pretty_thm ctxt) rules)
    47.8 +    Pretty.big_list "rules:" (map (Display.pretty_thm ctxt) rules)
    47.9      |> Pretty.string_of |> tracing
   47.10    else ();
   47.11  
    48.1 --- a/src/Pure/Isar/obtain.ML	Wed Jul 22 10:49:26 2009 +0200
    48.2 +++ b/src/Pure/Isar/obtain.ML	Wed Jul 22 11:23:09 2009 +0200
    48.3 @@ -180,9 +180,9 @@
    48.4      [prem] =>
    48.5        if Thm.concl_of th aconv thesis andalso
    48.6          Logic.strip_assums_concl prem aconv thesis then th
    48.7 -      else error ("Guessed a different clause:\n" ^ ProofContext.string_of_thm ctxt th)
    48.8 +      else error ("Guessed a different clause:\n" ^ Display.string_of_thm ctxt th)
    48.9    | [] => error "Goal solved -- nothing guessed."
   48.10 -  | _ => error ("Guess split into several cases:\n" ^ ProofContext.string_of_thm ctxt th));
   48.11 +  | _ => error ("Guess split into several cases:\n" ^ Display.string_of_thm ctxt th));
   48.12  
   48.13  fun result tac facts ctxt =
   48.14    let
   48.15 @@ -218,7 +218,7 @@
   48.16      val string_of_typ = Syntax.string_of_typ ctxt;
   48.17      val string_of_term = setmp show_types true (Syntax.string_of_term ctxt);
   48.18  
   48.19 -    fun err msg th = error (msg ^ ":\n" ^ ProofContext.string_of_thm ctxt th);
   48.20 +    fun err msg th = error (msg ^ ":\n" ^ Display.string_of_thm ctxt th);
   48.21  
   48.22      val maxidx = fold (Term.maxidx_typ o snd o fst) vars ~1;
   48.23      val rule = Thm.incr_indexes (maxidx + 1) raw_rule;
    49.1 --- a/src/Pure/Isar/proof.ML	Wed Jul 22 10:49:26 2009 +0200
    49.2 +++ b/src/Pure/Isar/proof.ML	Wed Jul 22 11:23:09 2009 +0200
    49.3 @@ -318,11 +318,11 @@
    49.4  val show_main_goal = ref false;
    49.5  val verbose = ProofContext.verbose;
    49.6  
    49.7 -val pretty_goals_local = Display.pretty_goals_aux o Syntax.pp;
    49.8 +val pretty_goals_local = Display_Goal.pretty_goals_aux o Syntax.pp;
    49.9  
   49.10  fun pretty_facts _ _ NONE = []
   49.11    | pretty_facts s ctxt (SOME ths) =
   49.12 -      [Pretty.big_list (s ^ "this:") (map (ProofContext.pretty_thm ctxt) ths), Pretty.str ""];
   49.13 +      [Pretty.big_list (s ^ "this:") (map (Display.pretty_thm ctxt) ths), Pretty.str ""];
   49.14  
   49.15  fun pretty_state nr state =
   49.16    let
   49.17 @@ -470,7 +470,7 @@
   49.18    let
   49.19      val thy = ProofContext.theory_of ctxt;
   49.20      val string_of_term = Syntax.string_of_term ctxt;
   49.21 -    val string_of_thm = ProofContext.string_of_thm ctxt;
   49.22 +    val string_of_thm = Display.string_of_thm ctxt;
   49.23  
   49.24      val ngoals = Thm.nprems_of goal;
   49.25      val _ = ngoals = 0 orelse error (Pretty.string_of (Pretty.chunks
    50.1 --- a/src/Pure/Isar/proof_context.ML	Wed Jul 22 10:49:26 2009 +0200
    50.2 +++ b/src/Pure/Isar/proof_context.ML	Wed Jul 22 11:23:09 2009 +0200
    50.3 @@ -36,13 +36,8 @@
    50.4    val theory_result: (theory -> 'a * theory) -> Proof.context -> 'a * Proof.context
    50.5    val extern_fact: Proof.context -> string -> xstring
    50.6    val pretty_term_abbrev: Proof.context -> term -> Pretty.T
    50.7 -  val pretty_thm_aux: Proof.context -> bool -> thm -> Pretty.T
    50.8 -  val pretty_thms_aux: Proof.context -> bool -> thm list -> Pretty.T
    50.9    val pretty_fact_aux: Proof.context -> bool -> string * thm list -> Pretty.T
   50.10 -  val pretty_thm: Proof.context -> thm -> Pretty.T
   50.11 -  val pretty_thms: Proof.context -> thm list -> Pretty.T
   50.12    val pretty_fact: Proof.context -> string * thm list -> Pretty.T
   50.13 -  val string_of_thm: Proof.context -> thm -> string
   50.14    val read_typ: Proof.context -> string -> typ
   50.15    val read_typ_syntax: Proof.context -> string -> typ
   50.16    val read_typ_abbrev: Proof.context -> string -> typ
   50.17 @@ -293,31 +288,18 @@
   50.18  
   50.19  fun pretty_term_abbrev ctxt = Syntax.pretty_term (set_mode mode_abbrev ctxt);
   50.20  
   50.21 -fun pretty_thm_aux ctxt show_status th =
   50.22 -  let
   50.23 -    val flags = {quote = false, show_hyps = true, show_status = show_status};
   50.24 -    val asms = map Thm.term_of (Assumption.all_assms_of ctxt);
   50.25 -  in Display.pretty_thm_aux (Syntax.pp ctxt) flags asms th end;
   50.26 -
   50.27 -fun pretty_thms_aux ctxt flag [th] = pretty_thm_aux ctxt flag th
   50.28 -  | pretty_thms_aux ctxt flag ths =
   50.29 -      Pretty.blk (0, Pretty.fbreaks (map (pretty_thm_aux ctxt flag) ths));
   50.30 -
   50.31  fun pretty_fact_name ctxt a = Pretty.block
   50.32    [Pretty.markup (Markup.fact a) [Pretty.str (extern_fact ctxt a)], Pretty.str ":"];
   50.33  
   50.34 -fun pretty_fact_aux ctxt flag ("", ths) = pretty_thms_aux ctxt flag ths
   50.35 +fun pretty_fact_aux ctxt flag ("", ths) =
   50.36 +      Display.pretty_thms_aux ctxt flag ths
   50.37    | pretty_fact_aux ctxt flag (a, [th]) = Pretty.block
   50.38 -      [pretty_fact_name ctxt a, Pretty.brk 1, pretty_thm_aux ctxt flag th]
   50.39 +      [pretty_fact_name ctxt a, Pretty.brk 1, Display.pretty_thm_aux ctxt flag th]
   50.40    | pretty_fact_aux ctxt flag (a, ths) = Pretty.block
   50.41 -      (Pretty.fbreaks (pretty_fact_name ctxt a :: map (pretty_thm_aux ctxt flag) ths));
   50.42 +      (Pretty.fbreaks (pretty_fact_name ctxt a :: map (Display.pretty_thm_aux ctxt flag) ths));
   50.43  
   50.44 -fun pretty_thm ctxt = pretty_thm_aux ctxt true;
   50.45 -fun pretty_thms ctxt = pretty_thms_aux ctxt true;
   50.46  fun pretty_fact ctxt = pretty_fact_aux ctxt true;
   50.47  
   50.48 -val string_of_thm = Pretty.string_of oo pretty_thm;
   50.49 -
   50.50  
   50.51  
   50.52  (** prepare types **)
   50.53 @@ -1369,7 +1351,7 @@
   50.54        val suppressed = len - ! prems_limit;
   50.55        val prt_prems = if null prems then []
   50.56          else [Pretty.big_list "prems:" ((if suppressed <= 0 then [] else [Pretty.str "..."]) @
   50.57 -          map (pretty_thm ctxt) (Library.drop (suppressed, prems)))];
   50.58 +          map (Display.pretty_thm ctxt) (Library.drop (suppressed, prems)))];
   50.59      in prt_structs @ prt_fixes @ prt_prems end;
   50.60  
   50.61  
    51.1 --- a/src/Pure/Isar/proof_display.ML	Wed Jul 22 10:49:26 2009 +0200
    51.2 +++ b/src/Pure/Isar/proof_display.ML	Wed Jul 22 11:23:09 2009 +0200
    51.3 @@ -35,7 +35,7 @@
    51.4    let
    51.5      val thy = Thm.theory_of_thm th;
    51.6      val flags = {quote = true, show_hyps = false, show_status = true};
    51.7 -  in Display.pretty_thm_aux (Syntax.pp_global thy) flags [] th end;
    51.8 +  in Display.pretty_thm_raw (Syntax.pp_global thy) flags [] th end;
    51.9  
   51.10  val pp_typ = Pretty.quote oo Syntax.pretty_typ_global;
   51.11  val pp_term = Pretty.quote oo Syntax.pretty_term_global;
   51.12 @@ -68,7 +68,7 @@
   51.13  
   51.14  fun pretty_rule ctxt s thm =
   51.15    Pretty.block [Pretty.str (s ^ " attempt to solve goal by exported rule:"),
   51.16 -    Pretty.fbrk, ProofContext.pretty_thm_aux ctxt false thm];
   51.17 +    Pretty.fbrk, Display.pretty_thm_aux ctxt false thm];
   51.18  
   51.19  val string_of_rule = Pretty.string_of ooo pretty_rule;
   51.20  
    52.1 --- a/src/Pure/Isar/runtime.ML	Wed Jul 22 10:49:26 2009 +0200
    52.2 +++ b/src/Pure/Isar/runtime.ML	Wed Jul 22 11:23:09 2009 +0200
    52.3 @@ -75,7 +75,7 @@
    52.4        | exn_msg ctxt (exn as TERM (msg, ts)) = raised exn "TERM" (msg ::
    52.5              (if detailed then if_context ctxt Syntax.string_of_term ts else []))
    52.6        | exn_msg ctxt (exn as THM (msg, i, thms)) = raised exn ("THM " ^ string_of_int i) (msg ::
    52.7 -            (if detailed then if_context ctxt ProofContext.string_of_thm thms else []))
    52.8 +            (if detailed then if_context ctxt Display.string_of_thm thms else []))
    52.9        | exn_msg _ exn = raised exn (General.exnMessage exn) [];
   52.10    in exn_msg NONE e end;
   52.11  
    53.1 --- a/src/Pure/ML-Systems/exn.ML	Wed Jul 22 10:49:26 2009 +0200
    53.2 +++ b/src/Pure/ML-Systems/exn.ML	Wed Jul 22 11:23:09 2009 +0200
    53.3 @@ -13,6 +13,8 @@
    53.4    val release: 'a result -> 'a
    53.5    exception Interrupt
    53.6    exception EXCEPTIONS of exn list
    53.7 +  val flatten: exn -> exn list
    53.8 +  val flatten_list: exn list -> exn list
    53.9    val release_all: 'a result list -> 'a list
   53.10    val release_first: 'a result list -> 'a list
   53.11  end;
   53.12 @@ -43,19 +45,15 @@
   53.13  exception Interrupt = Interrupt;
   53.14  exception EXCEPTIONS of exn list;
   53.15  
   53.16 -fun plain_exns (Result _) = []
   53.17 -  | plain_exns (Exn Interrupt) = []
   53.18 -  | plain_exns (Exn (EXCEPTIONS exns)) = List.concat (map (plain_exns o Exn) exns)
   53.19 -  | plain_exns (Exn exn) = [exn];
   53.20 -
   53.21 +fun flatten Interrupt = []
   53.22 +  | flatten (EXCEPTIONS exns) = flatten_list exns
   53.23 +  | flatten exn = [exn]
   53.24 +and flatten_list exns = List.concat (map flatten exns);
   53.25  
   53.26  fun release_all results =
   53.27    if List.all (fn Result _ => true | _ => false) results
   53.28    then map (fn Result x => x) results
   53.29 -  else
   53.30 -    (case List.concat (map plain_exns results) of
   53.31 -      [] => raise Interrupt
   53.32 -    | exns => raise EXCEPTIONS exns);
   53.33 +  else raise EXCEPTIONS (flatten_list (List.mapPartial get_exn results));
   53.34  
   53.35  fun release_first results = release_all results
   53.36    handle EXCEPTIONS (exn :: _) => reraise exn;
    54.1 --- a/src/Pure/ML-Systems/multithreading_polyml.ML	Wed Jul 22 10:49:26 2009 +0200
    54.2 +++ b/src/Pure/ML-Systems/multithreading_polyml.ML	Wed Jul 22 11:23:09 2009 +0200
    54.3 @@ -92,10 +92,12 @@
    54.4      val _ = Thread.setAttributes orig_atts;
    54.5    in Exn.release result end;
    54.6  
    54.7 -fun interruptible f = with_attributes regular_interrupts (fn _ => f);
    54.8 +fun interruptible f =
    54.9 +  with_attributes regular_interrupts (fn _ => fn x => f x);
   54.10  
   54.11  fun uninterruptible f =
   54.12 -  with_attributes no_interrupts (fn atts => f (fn g => with_attributes atts (fn _ => g)));
   54.13 +  with_attributes no_interrupts (fn atts => fn x =>
   54.14 +    f (fn g => with_attributes atts (fn _ => fn y => g y)) x);
   54.15  
   54.16  
   54.17  (* execution with time limit *)
    55.1 --- a/src/Pure/Proof/reconstruct.ML	Wed Jul 22 10:49:26 2009 +0200
    55.2 +++ b/src/Pure/Proof/reconstruct.ML	Wed Jul 22 11:23:09 2009 +0200
    55.3 @@ -255,7 +255,7 @@
    55.4        let
    55.5          fun search env [] = error ("Unsolvable constraints:\n" ^
    55.6                Pretty.string_of (Pretty.chunks (map (fn (_, p, _) =>
    55.7 -                Display.pretty_flexpair (Syntax.pp_global thy) (pairself
    55.8 +                Display_Goal.pretty_flexpair (Syntax.pp_global thy) (pairself
    55.9                    (Envir.norm_term bigenv) p)) cs)))
   55.10            | search env ((u, p as (t1, t2), vs)::ps) =
   55.11                if u then
    56.1 --- a/src/Pure/ProofGeneral/proof_general_pgip.ML	Wed Jul 22 10:49:26 2009 +0200
    56.2 +++ b/src/Pure/ProofGeneral/proof_general_pgip.ML	Wed Jul 22 11:23:09 2009 +0200
    56.3 @@ -655,7 +655,7 @@
    56.4                                    text=[XML.Elem("pgml",[],
    56.5                                                   maps YXML.parse_body strings)] })
    56.6  
    56.7 -        fun string_of_thm th = Pretty.string_of (Display.pretty_thm_aux
    56.8 +        fun string_of_thm th = Pretty.string_of (Display.pretty_thm_raw
    56.9              (Syntax.pp_global (Thm.theory_of_thm th))
   56.10              {quote = false, show_hyps = false, show_status = true} [] th)
   56.11  
    57.1 --- a/src/Pure/ROOT.ML	Wed Jul 22 10:49:26 2009 +0200
    57.2 +++ b/src/Pure/ROOT.ML	Wed Jul 22 11:23:09 2009 +0200
    57.3 @@ -115,17 +115,18 @@
    57.4  use "more_thm.ML";
    57.5  use "facts.ML";
    57.6  use "pure_thy.ML";
    57.7 -use "display.ML";
    57.8  use "drule.ML";
    57.9  use "morphism.ML";
   57.10  use "variable.ML";
   57.11  use "conv.ML";
   57.12 +use "display_goal.ML";
   57.13  use "tctical.ML";
   57.14  use "search.ML";
   57.15  use "tactic.ML";
   57.16  use "meta_simplifier.ML";
   57.17  use "conjunction.ML";
   57.18  use "assumption.ML";
   57.19 +use "display.ML";
   57.20  use "goal.ML";
   57.21  use "axclass.ML";
   57.22  
    58.1 --- a/src/Pure/Thy/thy_info.ML	Wed Jul 22 10:49:26 2009 +0200
    58.2 +++ b/src/Pure/Thy/thy_info.ML	Wed Jul 22 11:23:09 2009 +0200
    58.3 @@ -23,6 +23,7 @@
    58.4    val get_parents: string -> string list
    58.5    val touch_thy: string -> unit
    58.6    val touch_child_thys: string -> unit
    58.7 +  val thy_ord: theory * theory -> order
    58.8    val remove_thy: string -> unit
    58.9    val kill_thy: string -> unit
   58.10    val provide_file: Path.T -> string -> unit
   58.11 @@ -33,7 +34,6 @@
   58.12    val use_thys: string list -> unit
   58.13    val use_thy: string -> unit
   58.14    val time_use_thy: string -> unit
   58.15 -  val thy_ord: theory * theory -> order
   58.16    val begin_theory: string -> string list -> (Path.T * bool) list -> bool -> theory
   58.17    val end_theory: theory -> unit
   58.18    val register_thy: string -> unit
   58.19 @@ -231,17 +231,36 @@
   58.20  end;
   58.21  
   58.22  
   58.23 -(* manage pending proofs *)
   58.24 +(* management data *)
   58.25 +
   58.26 +structure Management_Data = TheoryDataFun
   58.27 +(
   58.28 +  type T =
   58.29 +    Task_Queue.group option *   (*worker thread group*)
   58.30 +    int;                        (*abstract update time*)
   58.31 +  val empty = (NONE, 0);
   58.32 +  val copy = I;
   58.33 +  fun extend _ = empty;
   58.34 +  fun merge _ _ = empty;
   58.35 +);
   58.36 +
   58.37 +val thy_ord = int_ord o pairself (#2 o Management_Data.get);
   58.38 +
   58.39 +
   58.40 +(* pending proofs *)
   58.41  
   58.42  fun join_thy name =
   58.43    (case lookup_theory name of
   58.44 -    NONE => []
   58.45 +    NONE => ()
   58.46    | SOME thy => PureThy.join_proofs thy);
   58.47  
   58.48  fun cancel_thy name =
   58.49    (case lookup_theory name of
   58.50      NONE => ()
   58.51 -  | SOME thy => PureThy.cancel_proofs thy);
   58.52 +  | SOME thy =>
   58.53 +      (case #1 (Management_Data.get thy) of
   58.54 +        NONE => ()
   58.55 +      | SOME group => Future.cancel_group group));
   58.56  
   58.57  
   58.58  (* remove theory *)
   58.59 @@ -374,8 +393,7 @@
   58.60      val exns = tasks |> maps (fn (name, _) =>
   58.61        let
   58.62          val after_load = Future.join (the (Symtab.lookup futures name));
   58.63 -        val proof_exns = join_thy name;
   58.64 -        val _ = null proof_exns orelse raise Exn.EXCEPTIONS proof_exns;
   58.65 +        val _ = join_thy name;
   58.66          val _ = after_load ();
   58.67        in [] end handle exn => (kill_thy name; [exn]));
   58.68  
   58.69 @@ -509,20 +527,6 @@
   58.70  end;
   58.71  
   58.72  
   58.73 -(* update_time *)
   58.74 -
   58.75 -structure UpdateTime = TheoryDataFun
   58.76 -(
   58.77 -  type T = int;
   58.78 -  val empty = 0;
   58.79 -  val copy = I;
   58.80 -  fun extend _ = empty;
   58.81 -  fun merge _ _ = empty;
   58.82 -);
   58.83 -
   58.84 -val thy_ord = int_ord o pairself UpdateTime.get;
   58.85 -
   58.86 -
   58.87  (* begin / end theory *)
   58.88  
   58.89  fun begin_theory name parents uses int =
   58.90 @@ -542,7 +546,7 @@
   58.91      val update_time = (case deps of NONE => 0 | SOME {update_time, ...} => update_time);
   58.92      val update_time = if update_time > 0 then update_time else serial ();
   58.93      val theory' = theory
   58.94 -      |> UpdateTime.put update_time
   58.95 +      |> Management_Data.put (Future.worker_group (), update_time)
   58.96        |> Present.begin_theory update_time dir uses;
   58.97  
   58.98      val uses_now = map_filter (fn (x, true) => SOME x | _ => NONE) uses;
   58.99 @@ -569,7 +573,7 @@
  58.100      val _ = check_unfinished error name;
  58.101      val _ = touch_thy name;
  58.102      val master = #master (ThyLoad.deps_thy Path.current name);
  58.103 -    val upd_time = UpdateTime.get thy;
  58.104 +    val upd_time = #2 (Management_Data.get thy);
  58.105    in
  58.106      CRITICAL (fn () =>
  58.107       (change_deps name (Option.map
    59.1 --- a/src/Pure/Tools/find_theorems.ML	Wed Jul 22 10:49:26 2009 +0200
    59.2 +++ b/src/Pure/Tools/find_theorems.ML	Wed Jul 22 11:23:09 2009 +0200
    59.3 @@ -408,7 +408,7 @@
    59.4  
    59.5  fun pretty_thm ctxt (thmref, thm) = Pretty.block
    59.6    [Pretty.str (Facts.string_of_ref thmref), Pretty.str ":", Pretty.brk 1,
    59.7 -    ProofContext.pretty_thm ctxt thm];
    59.8 +    Display.pretty_thm ctxt thm];
    59.9  
   59.10  fun print_theorems ctxt opt_goal opt_limit rem_dups raw_criteria =
   59.11    let
    60.1 --- a/src/Pure/display.ML	Wed Jul 22 10:49:26 2009 +0200
    60.2 +++ b/src/Pure/display.ML	Wed Jul 22 11:23:09 2009 +0200
    60.3 @@ -1,34 +1,32 @@
    60.4  (*  Title:      Pure/display.ML
    60.5      Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
    60.6 -    Copyright   1993  University of Cambridge
    60.7 +    Author:     Makarius
    60.8  
    60.9 -Printing of theorems, goals, results etc.
   60.10 +Printing of theorems, results etc.
   60.11  *)
   60.12  
   60.13  signature BASIC_DISPLAY =
   60.14  sig
   60.15    val goals_limit: int ref
   60.16 +  val show_consts: bool ref
   60.17    val show_hyps: bool ref
   60.18    val show_tags: bool ref
   60.19 -  val show_consts: bool ref
   60.20  end;
   60.21  
   60.22  signature DISPLAY =
   60.23  sig
   60.24    include BASIC_DISPLAY
   60.25 -  val pretty_flexpair: Pretty.pp -> term * term -> Pretty.T
   60.26 -  val pretty_thm_aux: Pretty.pp -> {quote: bool, show_hyps: bool, show_status: bool} ->
   60.27 +  val pretty_thm_raw: Pretty.pp -> {quote: bool, show_hyps: bool, show_status: bool} ->
   60.28      term list -> thm -> Pretty.T
   60.29 -  val pretty_thm: thm -> Pretty.T
   60.30 -  val string_of_thm: thm -> string
   60.31 -  val pretty_thms: thm list -> Pretty.T
   60.32 -  val pretty_thm_sg: theory -> thm -> Pretty.T
   60.33 -  val pretty_thms_sg: theory -> thm list -> Pretty.T
   60.34 -  val print_thm: thm -> unit
   60.35 -  val print_thms: thm list -> unit
   60.36 -  val prth: thm -> thm
   60.37 -  val prthq: thm Seq.seq -> thm Seq.seq
   60.38 -  val prths: thm list -> thm list
   60.39 +  val pretty_thm_aux: Proof.context -> bool -> thm -> Pretty.T
   60.40 +  val pretty_thm: Proof.context -> thm -> Pretty.T
   60.41 +  val pretty_thm_global: theory -> thm -> Pretty.T
   60.42 +  val pretty_thm_without_context: thm -> Pretty.T
   60.43 +  val string_of_thm: Proof.context -> thm -> string
   60.44 +  val string_of_thm_global: theory -> thm -> string
   60.45 +  val string_of_thm_without_context: thm -> string
   60.46 +  val pretty_thms_aux: Proof.context -> bool -> thm list -> Pretty.T
   60.47 +  val pretty_thms: Proof.context -> thm list -> Pretty.T
   60.48    val pretty_ctyp: ctyp -> Pretty.T
   60.49    val string_of_ctyp: ctyp -> string
   60.50    val print_ctyp: ctyp -> unit
   60.51 @@ -37,27 +35,26 @@
   60.52    val print_cterm: cterm -> unit
   60.53    val print_syntax: theory -> unit
   60.54    val pretty_full_theory: bool -> theory -> Pretty.T list
   60.55 -  val pretty_goals_aux: Pretty.pp -> Markup.T -> bool * bool -> int -> thm -> Pretty.T list
   60.56 -  val pretty_goals: int -> thm -> Pretty.T list
   60.57 -  val print_goals: int -> thm -> unit
   60.58  end;
   60.59  
   60.60  structure Display: DISPLAY =
   60.61  struct
   60.62  
   60.63 +(** options **)
   60.64 +
   60.65 +val goals_limit = Display_Goal.goals_limit;
   60.66 +val show_consts = Display_Goal.show_consts;
   60.67 +
   60.68 +val show_hyps = ref false;      (*false: print meta-hypotheses as dots*)
   60.69 +val show_tags = ref false;      (*false: suppress tags*)
   60.70 +
   60.71 +
   60.72  
   60.73  (** print thm **)
   60.74  
   60.75 -val goals_limit = ref 10;       (*max number of goals to print*)
   60.76 -val show_hyps = ref false;      (*false: print meta-hypotheses as dots*)
   60.77 -val show_tags = ref false;      (*false: suppress tags*)
   60.78 -
   60.79  fun pretty_tag (name, arg) = Pretty.strs [name, quote arg];
   60.80  val pretty_tags = Pretty.list "[" "]" o map pretty_tag;
   60.81  
   60.82 -fun pretty_flexpair pp (t, u) = Pretty.block
   60.83 -  [Pretty.term pp t, Pretty.str " =?=", Pretty.brk 1, Pretty.term pp u];
   60.84 -
   60.85  fun display_status false _ = ""
   60.86    | display_status true th =
   60.87        let
   60.88 @@ -71,7 +68,7 @@
   60.89          else ""
   60.90        end;
   60.91  
   60.92 -fun pretty_thm_aux pp {quote, show_hyps = show_hyps', show_status} asms raw_th =
   60.93 +fun pretty_thm_raw pp {quote, show_hyps = show_hyps', show_status} asms raw_th =
   60.94    let
   60.95      val th = Thm.strip_shyps raw_th;
   60.96      val {hyps, tpairs, prop, ...} = Thm.rep_thm th;
   60.97 @@ -89,7 +86,7 @@
   60.98        if hlen = 0 andalso status = "" then []
   60.99        else if ! show_hyps orelse show_hyps' then
  60.100          [Pretty.brk 2, Pretty.list "[" "]"
  60.101 -          (map (q o pretty_flexpair pp) tpairs @ map prt_term hyps' @
  60.102 +          (map (q o Display_Goal.pretty_flexpair pp) tpairs @ map prt_term hyps' @
  60.103             map (Pretty.sort pp) xshyps @
  60.104              (if status = "" then [] else [Pretty.str status]))]
  60.105        else [Pretty.brk 2, Pretty.str ("[" ^ implode (replicate hlen ".") ^ status ^ "]")];
  60.106 @@ -98,27 +95,33 @@
  60.107        else [Pretty.brk 1, pretty_tags tags];
  60.108    in Pretty.block (prt_term prop :: (hsymbs @ tsymbs)) end;
  60.109  
  60.110 -fun pretty_thm th =
  60.111 -  pretty_thm_aux (Syntax.pp_global (Thm.theory_of_thm th))
  60.112 -    {quote = true, show_hyps = false, show_status = true} [] th;
  60.113 -
  60.114 -val string_of_thm = Pretty.string_of o pretty_thm;
  60.115 -
  60.116 -fun pretty_thms [th] = pretty_thm th
  60.117 -  | pretty_thms ths = Pretty.block (Pretty.fbreaks (map pretty_thm ths));
  60.118 -
  60.119 -val pretty_thm_sg = pretty_thm oo Thm.transfer;
  60.120 -val pretty_thms_sg = pretty_thms oo (map o Thm.transfer);
  60.121 +fun pretty_thm_aux ctxt show_status th =
  60.122 +  let
  60.123 +    val flags = {quote = false, show_hyps = true, show_status = show_status};
  60.124 +    val asms = map Thm.term_of (Assumption.all_assms_of ctxt);
  60.125 +  in pretty_thm_raw (Syntax.pp ctxt) flags asms th end;
  60.126  
  60.127  
  60.128 -(* top-level commands for printing theorems *)
  60.129 +fun pretty_thm ctxt = pretty_thm_aux ctxt true;
  60.130 +
  60.131 +fun pretty_thm_global thy th =
  60.132 +  pretty_thm_raw (Syntax.pp_global thy)
  60.133 +    {quote = false, show_hyps = false, show_status = true} [] th;
  60.134 +
  60.135 +fun pretty_thm_without_context th = pretty_thm_global (Thm.theory_of_thm th) th;
  60.136  
  60.137 -val print_thm = Pretty.writeln o pretty_thm;
  60.138 -val print_thms = Pretty.writeln o pretty_thms;
  60.139 +val string_of_thm = Pretty.string_of oo pretty_thm;
  60.140 +val string_of_thm_global = Pretty.string_of oo pretty_thm_global;
  60.141 +val string_of_thm_without_context = Pretty.string_of o pretty_thm_without_context;
  60.142 +
  60.143  
  60.144 -fun prth th = (print_thm th; th);
  60.145 -fun prthq thq = (Seq.print (K print_thm) 100000 thq; thq);
  60.146 -fun prths ths = (prthq (Seq.of_list ths); ths);
  60.147 +(* multiple theorems *)
  60.148 +
  60.149 +fun pretty_thms_aux ctxt flag [th] = pretty_thm_aux ctxt flag th
  60.150 +  | pretty_thms_aux ctxt flag ths =
  60.151 +      Pretty.blk (0, Pretty.fbreaks (map (pretty_thm_aux ctxt flag) ths));
  60.152 +
  60.153 +fun pretty_thms ctxt = pretty_thms_aux ctxt true;
  60.154  
  60.155  
  60.156  (* other printing commands *)
  60.157 @@ -242,109 +245,7 @@
  60.158           Pretty.big_list "pattern restrictions:" (map pretty_restrict rests)]]
  60.159    end;
  60.160  
  60.161 -
  60.162 -
  60.163 -(** print_goals **)
  60.164 -
  60.165 -(* print_goals etc. *)
  60.166 -
  60.167 -val show_consts = ref false;  (*true: show consts with types in proof state output*)
  60.168 -
  60.169 -
  60.170 -(*print thm A1,...,An/B in "goal style" -- premises as numbered subgoals*)
  60.171 -
  60.172 -local
  60.173 -
  60.174 -fun ins_entry (x, y) =
  60.175 -  AList.default (op =) (x, []) #>
  60.176 -  AList.map_entry (op =) x (insert (op =) y);
  60.177 -
  60.178 -val add_consts = Term.fold_aterms
  60.179 -  (fn Const (c, T) => ins_entry (T, (c, T))
  60.180 -    | _ => I);
  60.181 -
  60.182 -val add_vars = Term.fold_aterms
  60.183 -  (fn Free (x, T) => ins_entry (T, (x, ~1))
  60.184 -    | Var (xi, T) => ins_entry (T, xi)
  60.185 -    | _ => I);
  60.186 -
  60.187 -val add_varsT = Term.fold_atyps
  60.188 -  (fn TFree (x, S) => ins_entry (S, (x, ~1))
  60.189 -    | TVar (xi, S) => ins_entry (S, xi)
  60.190 -    | _ => I);
  60.191 -
  60.192 -fun sort_idxs vs = map (apsnd (sort (prod_ord string_ord int_ord))) vs;
  60.193 -fun sort_cnsts cs = map (apsnd (sort_wrt fst)) cs;
  60.194 -
  60.195 -fun consts_of t = sort_cnsts (add_consts t []);
  60.196 -fun vars_of t = sort_idxs (add_vars t []);
  60.197 -fun varsT_of t = rev (sort_idxs (Term.fold_types add_varsT t []));
  60.198 -
  60.199 -in
  60.200 -
  60.201 -fun pretty_goals_aux pp markup (msg, main) maxgoals state =
  60.202 -  let
  60.203 -    fun prt_atoms prt prtT (X, xs) = Pretty.block
  60.204 -      [Pretty.block (Pretty.commas (map prt xs)), Pretty.str " ::",
  60.205 -        Pretty.brk 1, prtT X];
  60.206 -
  60.207 -    fun prt_var (x, ~1) = Pretty.term pp (Syntax.free x)
  60.208 -      | prt_var xi = Pretty.term pp (Syntax.var xi);
  60.209 -
  60.210 -    fun prt_varT (x, ~1) = Pretty.typ pp (TFree (x, []))
  60.211 -      | prt_varT xi = Pretty.typ pp (TVar (xi, []));
  60.212 -
  60.213 -    val prt_consts = prt_atoms (Pretty.term pp o Const) (Pretty.typ pp);
  60.214 -    val prt_vars = prt_atoms prt_var (Pretty.typ pp);
  60.215 -    val prt_varsT = prt_atoms prt_varT (Pretty.sort pp);
  60.216 -
  60.217 -
  60.218 -    fun pretty_list _ _ [] = []
  60.219 -      | pretty_list name prt lst = [Pretty.big_list name (map prt lst)];
  60.220 -
  60.221 -    fun pretty_subgoal (n, A) = Pretty.markup markup
  60.222 -      [Pretty.str (" " ^ string_of_int n ^ ". "), Pretty.term pp A];
  60.223 -    fun pretty_subgoals As = map pretty_subgoal (1 upto length As ~~ As);
  60.224 -
  60.225 -    val pretty_ffpairs = pretty_list "flex-flex pairs:" (pretty_flexpair pp);
  60.226 -
  60.227 -    val pretty_consts = pretty_list "constants:" prt_consts o consts_of;
  60.228 -    val pretty_vars = pretty_list "variables:" prt_vars o vars_of;
  60.229 -    val pretty_varsT = pretty_list "type variables:" prt_varsT o varsT_of;
  60.230 -
  60.231 -
  60.232 -    val {prop, tpairs, ...} = Thm.rep_thm state;
  60.233 -    val (As, B) = Logic.strip_horn prop;
  60.234 -    val ngoals = length As;
  60.235 -
  60.236 -    fun pretty_gs (types, sorts) =
  60.237 -      (if main then [Pretty.term pp B] else []) @
  60.238 -       (if ngoals = 0 then [Pretty.str "No subgoals!"]
  60.239 -        else if ngoals > maxgoals then
  60.240 -          pretty_subgoals (Library.take (maxgoals, As)) @
  60.241 -          (if msg then [Pretty.str ("A total of " ^ string_of_int ngoals ^ " subgoals...")]
  60.242 -           else [])
  60.243 -        else pretty_subgoals As) @
  60.244 -      pretty_ffpairs tpairs @
  60.245 -      (if ! show_consts then pretty_consts prop else []) @
  60.246 -      (if types then pretty_vars prop else []) @
  60.247 -      (if sorts then pretty_varsT prop else []);
  60.248 -  in
  60.249 -    setmp show_no_free_types true
  60.250 -      (setmp show_types (! show_types orelse ! show_sorts orelse ! show_all_types)
  60.251 -        (setmp show_sorts false pretty_gs))
  60.252 -   (! show_types orelse ! show_sorts orelse ! show_all_types, ! show_sorts)
  60.253 -  end;
  60.254 -
  60.255 -fun pretty_goals n th =
  60.256 -  pretty_goals_aux (Syntax.pp_global (Thm.theory_of_thm th)) Markup.none (true, true) n th;
  60.257 -
  60.258 -val print_goals = (Pretty.writeln o Pretty.chunks) oo pretty_goals;
  60.259 -
  60.260  end;
  60.261  
  60.262 -
  60.263 -end;
  60.264 -
  60.265 -structure BasicDisplay: BASIC_DISPLAY = Display;
  60.266 -open BasicDisplay;
  60.267 +structure Basic_Display: BASIC_DISPLAY = Display;
  60.268 +open Basic_Display;
    61.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
    61.2 +++ b/src/Pure/display_goal.ML	Wed Jul 22 11:23:09 2009 +0200
    61.3 @@ -0,0 +1,121 @@
    61.4 +(*  Title:      Pure/display_goal.ML
    61.5 +    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
    61.6 +    Author:     Makarius
    61.7 +
    61.8 +Display tactical goal state.
    61.9 +*)
   61.10 +
   61.11 +signature DISPLAY_GOAL =
   61.12 +sig
   61.13 +  val goals_limit: int ref
   61.14 +  val show_consts: bool ref
   61.15 +  val pretty_flexpair: Pretty.pp -> term * term -> Pretty.T
   61.16 +  val pretty_goals_aux: Pretty.pp -> Markup.T -> bool * bool -> int -> thm -> Pretty.T list
   61.17 +  val pretty_goals: int -> thm -> Pretty.T list
   61.18 +  val print_goals: int -> thm -> unit
   61.19 +end;
   61.20 +
   61.21 +structure Display_Goal: DISPLAY_GOAL =
   61.22 +struct
   61.23 +
   61.24 +val goals_limit = ref 10;      (*max number of goals to print*)
   61.25 +val show_consts = ref false;   (*true: show consts with types in proof state output*)
   61.26 +
   61.27 +fun pretty_flexpair pp (t, u) = Pretty.block
   61.28 +  [Pretty.term pp t, Pretty.str " =?=", Pretty.brk 1, Pretty.term pp u];
   61.29 +
   61.30 +
   61.31 +(*print thm A1,...,An/B in "goal style" -- premises as numbered subgoals*)
   61.32 +
   61.33 +local
   61.34 +
   61.35 +fun ins_entry (x, y) =
   61.36 +  AList.default (op =) (x, []) #>
   61.37 +  AList.map_entry (op =) x (insert (op =) y);
   61.38 +
   61.39 +val add_consts = Term.fold_aterms
   61.40 +  (fn Const (c, T) => ins_entry (T, (c, T))
   61.41 +    | _ => I);
   61.42 +
   61.43 +val add_vars = Term.fold_aterms
   61.44 +  (fn Free (x, T) => ins_entry (T, (x, ~1))
   61.45 +    | Var (xi, T) => ins_entry (T, xi)
   61.46 +    | _ => I);
   61.47 +
   61.48 +val add_varsT = Term.fold_atyps
   61.49 +  (fn TFree (x, S) => ins_entry (S, (x, ~1))
   61.50 +    | TVar (xi, S) => ins_entry (S, xi)
   61.51 +    | _ => I);
   61.52 +
   61.53 +fun sort_idxs vs = map (apsnd (sort (prod_ord string_ord int_ord))) vs;
   61.54 +fun sort_cnsts cs = map (apsnd (sort_wrt fst)) cs;
   61.55 +
   61.56 +fun consts_of t = sort_cnsts (add_consts t []);
   61.57 +fun vars_of t = sort_idxs (add_vars t []);
   61.58 +fun varsT_of t = rev (sort_idxs (Term.fold_types add_varsT t []));
   61.59 +
   61.60 +in
   61.61 +
   61.62 +fun pretty_goals_aux pp markup (msg, main) maxgoals state =
   61.63 +  let
   61.64 +    fun prt_atoms prt prtT (X, xs) = Pretty.block
   61.65 +      [Pretty.block (Pretty.commas (map prt xs)), Pretty.str " ::",
   61.66 +        Pretty.brk 1, prtT X];
   61.67 +
   61.68 +    fun prt_var (x, ~1) = Pretty.term pp (Syntax.free x)
   61.69 +      | prt_var xi = Pretty.term pp (Syntax.var xi);
   61.70 +
   61.71 +    fun prt_varT (x, ~1) = Pretty.typ pp (TFree (x, []))
   61.72 +      | prt_varT xi = Pretty.typ pp (TVar (xi, []));
   61.73 +
   61.74 +    val prt_consts = prt_atoms (Pretty.term pp o Const) (Pretty.typ pp);
   61.75 +    val prt_vars = prt_atoms prt_var (Pretty.typ pp);
   61.76 +    val prt_varsT = prt_atoms prt_varT (Pretty.sort pp);
   61.77 +
   61.78 +
   61.79 +    fun pretty_list _ _ [] = []
   61.80 +      | pretty_list name prt lst = [Pretty.big_list name (map prt lst)];
   61.81 +
   61.82 +    fun pretty_subgoal (n, A) = Pretty.markup markup
   61.83 +      [Pretty.str (" " ^ string_of_int n ^ ". "), Pretty.term pp A];
   61.84 +    fun pretty_subgoals As = map pretty_subgoal (1 upto length As ~~ As);
   61.85 +
   61.86 +    val pretty_ffpairs = pretty_list "flex-flex pairs:" (pretty_flexpair pp);
   61.87 +
   61.88 +    val pretty_consts = pretty_list "constants:" prt_consts o consts_of;
   61.89 +    val pretty_vars = pretty_list "variables:" prt_vars o vars_of;
   61.90 +    val pretty_varsT = pretty_list "type variables:" prt_varsT o varsT_of;
   61.91 +
   61.92 +
   61.93 +    val {prop, tpairs, ...} = Thm.rep_thm state;
   61.94 +    val (As, B) = Logic.strip_horn prop;
   61.95 +    val ngoals = length As;
   61.96 +
   61.97 +    fun pretty_gs (types, sorts) =
   61.98 +      (if main then [Pretty.term pp B] else []) @
   61.99 +       (if ngoals = 0 then [Pretty.str "No subgoals!"]
  61.100 +        else if ngoals > maxgoals then
  61.101 +          pretty_subgoals (Library.take (maxgoals, As)) @
  61.102 +          (if msg then [Pretty.str ("A total of " ^ string_of_int ngoals ^ " subgoals...")]
  61.103 +           else [])
  61.104 +        else pretty_subgoals As) @
  61.105 +      pretty_ffpairs tpairs @
  61.106 +      (if ! show_consts then pretty_consts prop else []) @
  61.107 +      (if types then pretty_vars prop else []) @
  61.108 +      (if sorts then pretty_varsT prop else []);
  61.109 +  in
  61.110 +    setmp show_no_free_types true
  61.111 +      (setmp show_types (! show_types orelse ! show_sorts orelse ! show_all_types)
  61.112 +        (setmp show_sorts false pretty_gs))
  61.113 +   (! show_types orelse ! show_sorts orelse ! show_all_types, ! show_sorts)
  61.114 +  end;
  61.115 +
  61.116 +fun pretty_goals n th =
  61.117 +  pretty_goals_aux (Syntax.pp_global (Thm.theory_of_thm th)) Markup.none (true, true) n th;
  61.118 +
  61.119 +val print_goals = (Pretty.writeln o Pretty.chunks) oo pretty_goals;
  61.120 +
  61.121 +end;
  61.122 +
  61.123 +end;
  61.124 +
    62.1 --- a/src/Pure/goal.ML	Wed Jul 22 10:49:26 2009 +0200
    62.2 +++ b/src/Pure/goal.ML	Wed Jul 22 11:23:09 2009 +0200
    62.3 @@ -78,7 +78,7 @@
    62.4    (case Thm.nprems_of th of
    62.5      0 => conclude th
    62.6    | n => raise THM ("Proof failed.\n" ^
    62.7 -      Pretty.string_of (Pretty.chunks (Display.pretty_goals n th)) ^
    62.8 +      Pretty.string_of (Pretty.chunks (Display_Goal.pretty_goals n th)) ^
    62.9        ("\n" ^ string_of_int n ^ " unsolved goal(s)!"), 0, [th]));
   62.10  
   62.11  
    63.1 --- a/src/Pure/old_goals.ML	Wed Jul 22 10:49:26 2009 +0200
    63.2 +++ b/src/Pure/old_goals.ML	Wed Jul 22 11:23:09 2009 +0200
    63.3 @@ -135,7 +135,7 @@
    63.4  (*Default action is to print an error message; could be suppressed for
    63.5    special applications.*)
    63.6  fun result_error_default state msg : thm =
    63.7 -  Pretty.str "Bad final proof state:" :: Display.pretty_goals (!goals_limit) state @
    63.8 +  Pretty.str "Bad final proof state:" :: Display_Goal.pretty_goals (!goals_limit) state @
    63.9      [Pretty.str msg, Pretty.str "Proof failed!"] |> Pretty.chunks |> Pretty.string_of |> error;
   63.10  
   63.11  val result_error_fn = ref result_error_default;
   63.12 @@ -199,7 +199,7 @@
   63.13    case e of
   63.14       THM (msg,i,thms) =>
   63.15           (writeln ("Exception THM " ^ string_of_int i ^ " raised:\n" ^ msg);
   63.16 -          List.app Display.print_thm thms)
   63.17 +          List.app (writeln o Display.string_of_thm_global thy) thms)
   63.18     | THEORY (msg,thys) =>
   63.19           (writeln ("Exception THEORY raised:\n" ^ msg);
   63.20            List.app (writeln o Context.str_of_thy) thys)
   63.21 @@ -277,7 +277,7 @@
   63.22        (if ngoals > 0 then " (" ^ string_of_int ngoals ^ " subgoal" ^
   63.23          (if ngoals <> 1 then "s" else "") ^ ")"
   63.24        else ""))] @
   63.25 -    Display.pretty_goals m th
   63.26 +    Display_Goal.pretty_goals m th
   63.27    end |> Pretty.chunks |> Pretty.writeln;
   63.28  
   63.29  (*Printing can raise exceptions, so the assignment occurs last.
    64.1 --- a/src/Pure/proofterm.ML	Wed Jul 22 10:49:26 2009 +0200
    64.2 +++ b/src/Pure/proofterm.ML	Wed Jul 22 11:23:09 2009 +0200
    64.3 @@ -37,10 +37,8 @@
    64.4  
    64.5    type oracle = string * term
    64.6    type pthm = serial * (string * term * proof_body future)
    64.7 -  val join_body: proof_body future ->
    64.8 -    {oracles: oracle OrdList.T, thms: pthm OrdList.T, proof: proof}
    64.9 +  val proof_of: proof_body -> proof
   64.10    val join_proof: proof_body future -> proof
   64.11 -  val proof_of: proof_body -> proof
   64.12    val fold_proof_atoms: bool -> (proof -> 'a -> 'a) -> proof list -> 'a -> 'a
   64.13    val fold_body_thms: (string * term * proof_body -> 'a -> 'a) -> proof_body list -> 'a -> 'a
   64.14    val join_bodies: proof_body list -> unit
   64.15 @@ -152,10 +150,8 @@
   64.16  type oracle = string * term;
   64.17  type pthm = serial * (string * term * proof_body future);
   64.18  
   64.19 -val join_body = Future.join #> (fn PBody args => args);
   64.20 -val join_proof = #proof o join_body;
   64.21 -
   64.22  fun proof_of (PBody {proof, ...}) = proof;
   64.23 +val join_proof = Future.join #> proof_of;
   64.24  
   64.25  
   64.26  (***** proof atoms *****)
   64.27 @@ -177,13 +173,15 @@
   64.28  
   64.29  fun fold_body_thms f =
   64.30    let
   64.31 -    fun app (PBody {thms, ...}) = thms |> fold (fn (i, (name, prop, body)) => fn (x, seen) =>
   64.32 -      if Inttab.defined seen i then (x, seen)
   64.33 -      else
   64.34 -        let
   64.35 -          val body' = Future.join body;
   64.36 -          val (x', seen') = app body' (x, Inttab.update (i, ()) seen);
   64.37 -        in (f (name, prop, body') x', seen') end);
   64.38 +    fun app (PBody {thms, ...}) =
   64.39 +     (Future.join_results (map (#3 o #2) thms);
   64.40 +      thms |> fold (fn (i, (name, prop, body)) => fn (x, seen) =>
   64.41 +        if Inttab.defined seen i then (x, seen)
   64.42 +        else
   64.43 +          let
   64.44 +            val body' = Future.join body;
   64.45 +            val (x', seen') = app body' (x, Inttab.update (i, ()) seen);
   64.46 +          in (f (name, prop, body') x', seen') end));
   64.47    in fn bodies => fn x => #1 (fold app bodies (x, Inttab.empty)) end;
   64.48  
   64.49  fun join_bodies bodies = fold_body_thms (fn _ => fn () => ()) bodies ();
   64.50 @@ -223,13 +221,14 @@
   64.51  val all_oracles_of =
   64.52    let
   64.53      fun collect (PBody {oracles, thms, ...}) =
   64.54 +     (Future.join_results (map (#3 o #2) thms);
   64.55        thms |> fold (fn (i, (_, _, body)) => fn (x, seen) =>
   64.56          if Inttab.defined seen i then (x, seen)
   64.57          else
   64.58            let
   64.59              val body' = Future.join body;
   64.60              val (x', seen') = collect body' (x, Inttab.update (i, ()) seen);
   64.61 -          in (merge_oracles oracles x', seen') end);
   64.62 +          in (merge_oracles oracles x', seen') end));
   64.63    in fn body => #1 (collect body ([], Inttab.empty)) end;
   64.64  
   64.65  fun approximate_proof_body prf =
   64.66 @@ -1342,5 +1341,5 @@
   64.67  
   64.68  end;
   64.69  
   64.70 -structure BasicProofterm : BASIC_PROOFTERM = Proofterm;
   64.71 -open BasicProofterm;
   64.72 +structure Basic_Proofterm : BASIC_PROOFTERM = Proofterm;
   64.73 +open Basic_Proofterm;
    65.1 --- a/src/Pure/pure_thy.ML	Wed Jul 22 10:49:26 2009 +0200
    65.2 +++ b/src/Pure/pure_thy.ML	Wed Jul 22 11:23:09 2009 +0200
    65.3 @@ -10,8 +10,7 @@
    65.4    val intern_fact: theory -> xstring -> string
    65.5    val defined_fact: theory -> string -> bool
    65.6    val hide_fact: bool -> string -> theory -> theory
    65.7 -  val join_proofs: theory -> exn list
    65.8 -  val cancel_proofs: theory -> unit
    65.9 +  val join_proofs: theory -> unit
   65.10    val get_fact: Context.generic -> theory -> Facts.ref -> thm list
   65.11    val get_thms: theory -> xstring -> thm list
   65.12    val get_thm: theory -> xstring -> thm
   65.13 @@ -59,11 +58,11 @@
   65.14  
   65.15  structure FactsData = TheoryDataFun
   65.16  (
   65.17 -  type T = Facts.T * (unit lazy list * Task_Queue.group Inttab.table);
   65.18 -  val empty = (Facts.empty, ([], Inttab.empty));
   65.19 +  type T = Facts.T * thm list;
   65.20 +  val empty = (Facts.empty, []);
   65.21    val copy = I;
   65.22 -  fun extend (facts, _) = (facts, ([], Inttab.empty));
   65.23 -  fun merge _ ((facts1, _), (facts2, _)) = (Facts.merge (facts1, facts2), ([], Inttab.empty));
   65.24 +  fun extend (facts, _) = (facts, []);
   65.25 +  fun merge _ ((facts1, _), (facts2, _)) = (Facts.merge (facts1, facts2), []);
   65.26  );
   65.27  
   65.28  
   65.29 @@ -79,14 +78,9 @@
   65.30  
   65.31  (* proofs *)
   65.32  
   65.33 -fun lazy_proof thm = Lazy.lazy (fn () => Thm.join_proof thm);
   65.34 +fun register_proofs (thy, thms) = (FactsData.map (apsnd (append thms)) thy, thms);
   65.35  
   65.36 -fun join_proofs thy =
   65.37 -  map_filter (Exn.get_exn o Lazy.force_result) (rev (#1 (#2 (FactsData.get thy))));
   65.38 -
   65.39 -fun cancel_proofs thy =
   65.40 -  Inttab.fold (fn (_, group) => fn () => Future.cancel_group group)
   65.41 -    (#2 (#2 (FactsData.get thy))) ();
   65.42 +fun join_proofs thy = Thm.join_proofs (rev (#2 (FactsData.get thy)));
   65.43  
   65.44  
   65.45  
   65.46 @@ -146,24 +140,15 @@
   65.47  
   65.48  (* enter_thms *)
   65.49  
   65.50 -val pending_groups =
   65.51 -  Thm.promises_of #> fold (fn (_, future) =>
   65.52 -    if Future.is_finished future then I
   65.53 -    else Inttab.update (`Task_Queue.group_id (Future.group_of future)));
   65.54 -
   65.55 -fun enter_proofs (thy, thms) =
   65.56 -  (FactsData.map (apsnd (fn (proofs, groups) =>
   65.57 -    (fold (cons o lazy_proof) thms proofs, fold pending_groups thms groups))) thy, thms);
   65.58 -
   65.59  fun enter_thms pre_name post_name app_att (b, thms) thy =
   65.60    if Binding.is_empty b
   65.61 -  then swap (enter_proofs (app_att (thy, thms)))
   65.62 +  then swap (register_proofs (app_att (thy, thms)))
   65.63    else
   65.64      let
   65.65        val naming = Sign.naming_of thy;
   65.66        val name = NameSpace.full_name naming b;
   65.67        val (thy', thms') =
   65.68 -        enter_proofs (apsnd (post_name name) (app_att (thy, pre_name name thms)));
   65.69 +        register_proofs (apsnd (post_name name) (app_att (thy, pre_name name thms)));
   65.70        val thms'' = map (Thm.transfer thy') thms';
   65.71        val thy'' = thy' |> (FactsData.map o apfst) (Facts.add_global naming (b, thms'') #> snd);
   65.72      in (thms'', thy'') end;
    66.1 --- a/src/Pure/simplifier.ML	Wed Jul 22 10:49:26 2009 +0200
    66.2 +++ b/src/Pure/simplifier.ML	Wed Jul 22 11:23:09 2009 +0200
    66.3 @@ -79,7 +79,7 @@
    66.4  fun pretty_ss ctxt ss =
    66.5    let
    66.6      val pretty_cterm = Syntax.pretty_term ctxt o Thm.term_of;
    66.7 -    val pretty_thm = ProofContext.pretty_thm ctxt;
    66.8 +    val pretty_thm = Display.pretty_thm ctxt;
    66.9      fun pretty_proc (name, lhss) = Pretty.big_list (name ^ ":") (map pretty_cterm lhss);
   66.10      fun pretty_cong (name, thm) =
   66.11        Pretty.block [Pretty.str (name ^ ":"), Pretty.brk 1, pretty_thm thm];
    67.1 --- a/src/Pure/tctical.ML	Wed Jul 22 10:49:26 2009 +0200
    67.2 +++ b/src/Pure/tctical.ML	Wed Jul 22 11:23:09 2009 +0200
    67.3 @@ -195,7 +195,7 @@
    67.4      (fn st =>
    67.5       (tracing msg;
    67.6        tracing ((Pretty.string_of o Pretty.chunks o
    67.7 -                 Display.pretty_goals (! Display.goals_limit)) st);
    67.8 +                 Display_Goal.pretty_goals (! Display_Goal.goals_limit)) st);
    67.9        Seq.single st));
   67.10  
   67.11  (*Pause until a line is typed -- if non-empty then fail. *)
   67.12 @@ -233,7 +233,7 @@
   67.13  (*Extract from a tactic, a thm->thm seq function that handles tracing*)
   67.14  fun tracify flag tac st =
   67.15    if !flag andalso not (!suppress_tracing)
   67.16 -           then (Display.print_goals (! Display.goals_limit) st;
   67.17 +           then (Display_Goal.print_goals (! Display_Goal.goals_limit) st;
   67.18                   tracing "** Press RETURN to continue:";
   67.19                   exec_trace_command flag (tac,st))
   67.20    else tac st;
    68.1 --- a/src/Pure/thm.ML	Wed Jul 22 10:49:26 2009 +0200
    68.2 +++ b/src/Pure/thm.ML	Wed Jul 22 11:23:09 2009 +0200
    68.3 @@ -141,10 +141,9 @@
    68.4    val bicompose: bool -> bool * thm * int -> int -> thm -> thm Seq.seq
    68.5    val biresolution: bool -> (bool * thm) list -> int -> thm -> thm Seq.seq
    68.6    val rename_boundvars: term -> term -> thm -> thm
    68.7 +  val join_proofs: thm list -> unit
    68.8    val proof_body_of: thm -> proof_body
    68.9    val proof_of: thm -> proof
   68.10 -  val join_proof: thm -> unit
   68.11 -  val promises_of: thm -> (serial * thm future) list
   68.12    val status_of: thm -> {oracle: bool, unfinished: bool, failed: bool}
   68.13    val future: thm future -> cterm -> thm
   68.14    val get_name: thm -> string
   68.15 @@ -1612,18 +1611,18 @@
   68.16  fun raw_body (Thm (Deriv {body, ...}, _)) = body;
   68.17  
   68.18  fun fulfill_body (Thm (Deriv {promises, body}, {thy_ref, ...})) =
   68.19 -  let val ps = map (apsnd (fulfill_body o Future.join)) promises
   68.20 -  in Pt.fulfill_proof (Theory.deref thy_ref) ps body end;
   68.21 +  Pt.fulfill_proof (Theory.deref thy_ref)
   68.22 +    (map #1 promises ~~ fulfill_bodies (map #2 promises)) body
   68.23 +and fulfill_bodies futures = map fulfill_body (Exn.release_all (Future.join_results futures));
   68.24 +
   68.25 +val join_proofs = Pt.join_bodies o map fulfill_body;
   68.26  
   68.27  fun proof_body_of thm = (Pt.join_bodies [raw_body thm]; fulfill_body thm);
   68.28  val proof_of = Pt.proof_of o proof_body_of;
   68.29 -val join_proof = ignore o proof_body_of;
   68.30  
   68.31  
   68.32  (* derivation status *)
   68.33  
   68.34 -fun promises_of (Thm (Deriv {promises, ...}, _)) = promises;
   68.35 -
   68.36  fun status_of (Thm (Deriv {promises, body}, _)) =
   68.37    let
   68.38      val ps = map (Future.peek o snd) promises;
   68.39 @@ -1652,7 +1651,7 @@
   68.40      val _ = null hyps orelse err "bad hyps";
   68.41      val _ = Sorts.subset (shyps, orig_shyps) orelse err "bad shyps";
   68.42      val _ = forall (fn (j, _) => i <> j) promises orelse err "bad dependencies";
   68.43 -    val _ = List.app (ignore o fulfill_body o Future.join o #2) promises;
   68.44 +    val _ = fulfill_bodies (map #2 promises);
   68.45    in thm end;
   68.46  
   68.47  fun future future_thm ct =
   68.48 @@ -1743,5 +1742,5 @@
   68.49  
   68.50  end;
   68.51  
   68.52 -structure BasicThm: BASIC_THM = Thm;
   68.53 -open BasicThm;
   68.54 +structure Basic_Thm: BASIC_THM = Thm;
   68.55 +open Basic_Thm;
    69.1 --- a/src/Sequents/prover.ML	Wed Jul 22 10:49:26 2009 +0200
    69.2 +++ b/src/Sequents/prover.ML	Wed Jul 22 11:23:09 2009 +0200
    69.3 @@ -27,7 +27,8 @@
    69.4  
    69.5  fun warn_duplicates [] = []
    69.6    | warn_duplicates dups =
    69.7 -      (warning (cat_lines ("Ignoring duplicate theorems:" :: map Display.string_of_thm dups));
    69.8 +      (warning (cat_lines ("Ignoring duplicate theorems:" ::
    69.9 +          map Display.string_of_thm_without_context dups));
   69.10         dups);
   69.11  
   69.12  fun (Pack(safes,unsafes)) add_safes ths   = 
   69.13 @@ -50,8 +51,9 @@
   69.14  
   69.15  
   69.16  fun print_pack (Pack(safes,unsafes)) =
   69.17 -    (writeln "Safe rules:";  Display.print_thms safes;
   69.18 -     writeln "Unsafe rules:"; Display.print_thms unsafes);
   69.19 +  writeln (cat_lines
   69.20 +   (["Safe rules:"] @ map Display.string_of_thm_without_context safes @
   69.21 +    ["Unsafe rules:"] @ map Display.string_of_thm_without_context unsafes));
   69.22  
   69.23  (*Returns the list of all formulas in the sequent*)
   69.24  fun forms_of_seq (Const("SeqO'",_) $ P $ u) = P :: forms_of_seq u
    70.1 --- a/src/Sequents/simpdata.ML	Wed Jul 22 10:49:26 2009 +0200
    70.2 +++ b/src/Sequents/simpdata.ML	Wed Jul 22 11:23:09 2009 +0200
    70.3 @@ -40,7 +40,7 @@
    70.4                      | (Const("Not",_)$_)      => th RS @{thm iff_reflection_F}
    70.5                      | _                       => th RS @{thm iff_reflection_T})
    70.6             | _ => error ("addsimps: unable to use theorem\n" ^
    70.7 -                         Display.string_of_thm th));
    70.8 +                         Display.string_of_thm_without_context th));
    70.9  
   70.10  (*Replace premises x=y, X<->Y by X==Y*)
   70.11  val mk_meta_prems =
    71.1 --- a/src/Tools/Code/code_preproc.ML	Wed Jul 22 10:49:26 2009 +0200
    71.2 +++ b/src/Tools/Code/code_preproc.ML	Wed Jul 22 11:23:09 2009 +0200
    71.3 @@ -214,7 +214,7 @@
    71.4    |> map (fn (s, thms) =>
    71.5         (Pretty.block o Pretty.fbreaks) (
    71.6           Pretty.str s
    71.7 -         :: map (Display.pretty_thm o fst) thms
    71.8 +         :: map (Display.pretty_thm_global thy o fst) thms
    71.9         ))
   71.10    |> Pretty.chunks;
   71.11  
   71.12 @@ -529,7 +529,7 @@
   71.13        in
   71.14          Thm.transitive thm1 (Thm.transitive thm2 thm3) handle THM _ =>
   71.15            error ("could not construct evaluation proof:\n"
   71.16 -          ^ (cat_lines o map Display.string_of_thm) [thm1, thm2, thm3])
   71.17 +          ^ (cat_lines o map (Display.string_of_thm_global thy)) [thm1, thm2, thm3])
   71.18        end;
   71.19    in gen_eval thy I conclude_evaluation end;
   71.20  
    72.1 --- a/src/Tools/Code/code_printer.ML	Wed Jul 22 10:49:26 2009 +0200
    72.2 +++ b/src/Tools/Code/code_printer.ML	Wed Jul 22 11:23:09 2009 +0200
    72.3 @@ -82,7 +82,7 @@
    72.4  
    72.5  open Code_Thingol;
    72.6  
    72.7 -fun nerror thm s = error (s ^ ",\nin equation " ^ Display.string_of_thm thm);
    72.8 +fun nerror thm s = error (s ^ ",\nin equation " ^ Display.string_of_thm_without_context thm);
    72.9  
   72.10  (** assembling text pieces **)
   72.11  
    73.1 --- a/src/Tools/Code/code_thingol.ML	Wed Jul 22 10:49:26 2009 +0200
    73.2 +++ b/src/Tools/Code/code_thingol.ML	Wed Jul 22 11:23:09 2009 +0200
    73.3 @@ -469,7 +469,7 @@
    73.4    let
    73.5      val err_class = Sorts.class_error (Syntax.pp_global thy) e;
    73.6      val err_thm = case thm
    73.7 -     of SOME thm => "\n(in code equation " ^ Display.string_of_thm thm ^ ")" | NONE => "";
    73.8 +     of SOME thm => "\n(in code equation " ^ Display.string_of_thm_global thy thm ^ ")" | NONE => "";
    73.9      val err_typ = "Type " ^ Syntax.string_of_typ_global thy ty ^ " not of sort "
   73.10        ^ Syntax.string_of_sort_global thy sort;
   73.11    in error ("Wellsortedness error" ^ err_thm ^ ":\n" ^ err_typ ^ "\n" ^ err_class) end;
    74.1 --- a/src/Tools/coherent.ML	Wed Jul 22 10:49:26 2009 +0200
    74.2 +++ b/src/Tools/coherent.ML	Wed Jul 22 11:23:09 2009 +0200
    74.3 @@ -177,7 +177,7 @@
    74.4  fun thm_of_cl_prf thy goal asms (ClPrf (th, (tye, env), insts, is, prfs)) =
    74.5    let
    74.6      val _ = message (fn () => space_implode "\n"
    74.7 -      ("asms:" :: map Display.string_of_thm asms) ^ "\n\n");
    74.8 +      ("asms:" :: map (Display.string_of_thm_global thy) asms) ^ "\n\n");
    74.9      val th' = Drule.implies_elim_list
   74.10        (Thm.instantiate
   74.11           (map (fn (ixn, (S, T)) =>
    75.1 --- a/src/Tools/induct.ML	Wed Jul 22 10:49:26 2009 +0200
    75.2 +++ b/src/Tools/induct.ML	Wed Jul 22 11:23:09 2009 +0200
    75.3 @@ -124,7 +124,7 @@
    75.4  
    75.5  fun pretty_rules ctxt kind rs =
    75.6    let val thms = map snd (Item_Net.content rs)
    75.7 -  in Pretty.big_list kind (map (ProofContext.pretty_thm ctxt) thms) end;
    75.8 +  in Pretty.big_list kind (map (Display.pretty_thm ctxt) thms) end;
    75.9  
   75.10  
   75.11  (* context data *)
    76.1 --- a/src/ZF/Tools/inductive_package.ML	Wed Jul 22 10:49:26 2009 +0200
    76.2 +++ b/src/ZF/Tools/inductive_package.ML	Wed Jul 22 11:23:09 2009 +0200
    76.3 @@ -247,8 +247,7 @@
    76.4      (intr_tms, map intro_tacsf (mk_disj_rls (length intr_tms)))
    76.5      |> ListPair.map (fn (t, tacs) =>
    76.6        Goal.prove_global thy1 [] [] t
    76.7 -        (fn _ => EVERY (rewrite_goals_tac part_rec_defs :: tacs)))
    76.8 -    handle MetaSimplifier.SIMPLIFIER (msg, thm) => (Display.print_thm thm; error msg);
    76.9 +        (fn _ => EVERY (rewrite_goals_tac part_rec_defs :: tacs)));
   76.10  
   76.11    (********)
   76.12    val dummy = writeln "  Proving the elimination rule...";
   76.13 @@ -318,11 +317,12 @@
   76.14       val ind_prems = map (induct_prem (map (rpair pred) rec_tms))
   76.15                           intr_tms;
   76.16  
   76.17 -     val dummy = if !Ind_Syntax.trace then
   76.18 -                 (writeln "ind_prems = ";
   76.19 -                  List.app (writeln o Syntax.string_of_term ctxt1) ind_prems;
   76.20 -                  writeln "raw_induct = "; Display.print_thm raw_induct)
   76.21 -             else ();
   76.22 +     val dummy =
   76.23 +      if ! Ind_Syntax.trace then
   76.24 +        writeln (cat_lines
   76.25 +          (["ind_prems:"] @ map (Syntax.string_of_term ctxt1) ind_prems @
   76.26 +           ["raw_induct:", Display.string_of_thm ctxt1 raw_induct]))
   76.27 +      else ();
   76.28  
   76.29  
   76.30       (*We use a MINIMAL simpset. Even FOL_ss contains too many simpules.
   76.31 @@ -351,9 +351,10 @@
   76.32                                 ORELSE' bound_hyp_subst_tac)),
   76.33              ind_tac (rev (map (rewrite_rule part_rec_defs) prems)) (length prems)]);
   76.34  
   76.35 -     val dummy = if !Ind_Syntax.trace then
   76.36 -                 (writeln "quant_induct = "; Display.print_thm quant_induct)
   76.37 -             else ();
   76.38 +     val dummy =
   76.39 +      if ! Ind_Syntax.trace then
   76.40 +        writeln ("quant_induct:\n" ^ Display.string_of_thm ctxt1 quant_induct)
   76.41 +      else ();
   76.42  
   76.43  
   76.44       (*** Prove the simultaneous induction rule ***)
   76.45 @@ -426,9 +427,10 @@
   76.46                  REPEAT (rewrite_goals_tac [Pr.split_eq] THEN lemma_tac 1)]))
   76.47         else (writeln "  [ No mutual induction rule needed ]"; @{thm TrueI});
   76.48  
   76.49 -     val dummy = if !Ind_Syntax.trace then
   76.50 -                 (writeln "lemma = "; Display.print_thm lemma)
   76.51 -             else ();
   76.52 +     val dummy =
   76.53 +      if ! Ind_Syntax.trace then
   76.54 +        writeln ("lemma: " ^ Display.string_of_thm ctxt1 lemma)
   76.55 +      else ();
   76.56  
   76.57  
   76.58       (*Mutual induction follows by freeness of Inl/Inr.*)
    77.1 --- a/src/ZF/Tools/typechk.ML	Wed Jul 22 10:49:26 2009 +0200
    77.2 +++ b/src/ZF/Tools/typechk.ML	Wed Jul 22 11:23:09 2009 +0200
    77.3 @@ -27,7 +27,8 @@
    77.4  
    77.5  fun add_rule th (tcs as TC {rules, net}) =
    77.6    if member Thm.eq_thm_prop rules th then
    77.7 -    (warning ("Ignoring duplicate type-checking rule\n" ^ Display.string_of_thm th); tcs)
    77.8 +    (warning ("Ignoring duplicate type-checking rule\n" ^
    77.9 +        Display.string_of_thm_without_context th); tcs)
   77.10    else
   77.11      TC {rules = th :: rules,
   77.12          net = Net.insert_term (K false) (Thm.concl_of th, th) net};
   77.13 @@ -36,7 +37,8 @@
   77.14    if member Thm.eq_thm_prop rules th then
   77.15      TC {net = Net.delete_term Thm.eq_thm_prop (Thm.concl_of th, th) net,
   77.16          rules = remove Thm.eq_thm_prop th rules}
   77.17 -  else (warning ("No such type-checking rule\n" ^ Display.string_of_thm th); tcs);
   77.18 +  else (warning ("No such type-checking rule\n" ^
   77.19 +    Display.string_of_thm_without_context th); tcs);
   77.20  
   77.21  
   77.22  (* generic data *)
   77.23 @@ -60,7 +62,7 @@
   77.24  fun print_tcset ctxt =
   77.25    let val TC {rules, ...} = tcset_of ctxt in
   77.26      Pretty.writeln (Pretty.big_list "type-checking rules:"
   77.27 -      (map (ProofContext.pretty_thm ctxt) rules))
   77.28 +      (map (Display.pretty_thm ctxt) rules))
   77.29    end;
   77.30  
   77.31