# HG changeset patch
# User wenzelm
# Date 1285343732 -7200
# Node ID 1906c0c773415542b32e9a88ea2e01d2fef3722d
# Parent  e75b993c04334598330b7f460c77669820cf29ab# Parent  b88a6bc371de9ecebccc97a7f0532a882d7d6219
merged

diff -r e75b993c0433 -r 1906c0c77341 Admin/isatest/isatest-makeall
--- a/Admin/isatest/isatest-makeall	Fri Sep 24 15:53:57 2010 +0200
+++ b/Admin/isatest/isatest-makeall	Fri Sep 24 17:55:32 2010 +0200
@@ -146,6 +146,8 @@
 
     echo ------------------- starting test --- `date` --- $HOSTNAME > $TESTLOG 2>&1
 
+    echo "Isabelle version: $IDENT" >> $TESTLOG 2>&1
+
     if [ "${ISABELLE_HOME_USER:0:14}" == "/tmp/isabelle-" ]; then
         echo "--- cleaning up old $ISABELLE_HOME_USER"
         rm -rf $ISABELLE_HOME_USER
diff -r e75b993c0433 -r 1906c0c77341 NEWS
--- a/NEWS	Fri Sep 24 15:53:57 2010 +0200
+++ b/NEWS	Fri Sep 24 17:55:32 2010 +0200
@@ -68,7 +68,7 @@
 * Discontinued ancient 'constdefs' command.  INCOMPATIBILITY, use
 'definition' instead.
 
-* Document antiquotations 'class' and 'type' for printing classes
+* Document antiquotations @{class} and @{type} for printing classes
 and type constructors.
 
 
diff -r e75b993c0433 -r 1906c0c77341 doc-src/IsarImplementation/Thy/Prelim.thy
--- a/doc-src/IsarImplementation/Thy/Prelim.thy	Fri Sep 24 15:53:57 2010 +0200
+++ b/doc-src/IsarImplementation/Thy/Prelim.thy	Fri Sep 24 17:55:32 2010 +0200
@@ -432,30 +432,30 @@
 
   structure Terms = Theory_Data
   (
-    type T = term OrdList.T;
+    type T = term Ord_List.T;
     val empty = [];
     val extend = I;
     fun merge (ts1, ts2) =
-      OrdList.union Term_Ord.fast_term_ord ts1 ts2;
+      Ord_List.union Term_Ord.fast_term_ord ts1 ts2;
   )
 
   val get = Terms.get;
 
   fun add raw_t thy =
     let val t = Sign.cert_term thy raw_t
-    in Terms.map (OrdList.insert Term_Ord.fast_term_ord t) thy end;
+    in Terms.map (Ord_List.insert Term_Ord.fast_term_ord t) thy end;
 
   end;
 *}
 
-text {* We use @{ML_type "term OrdList.T"} for reasonably efficient
+text {* We use @{ML_type "term Ord_List.T"} for reasonably efficient
   representation of a set of terms: all operations are linear in the
   number of stored elements.  Here we assume that our users do not
   care about the declaration order, since that data structure forces
   its own arrangement of elements.
 
   Observe how the @{verbatim merge} operation joins the data slots of
-  the two constituents: @{ML OrdList.union} prevents duplication of
+  the two constituents: @{ML Ord_List.union} prevents duplication of
   common data from different branches, thus avoiding the danger of
   exponential blowup.  (Plain list append etc.\ must never be used for
   theory data merges.)
diff -r e75b993c0433 -r 1906c0c77341 doc-src/IsarImplementation/Thy/document/Prelim.tex
--- a/doc-src/IsarImplementation/Thy/document/Prelim.tex	Fri Sep 24 15:53:57 2010 +0200
+++ b/doc-src/IsarImplementation/Thy/document/Prelim.tex	Fri Sep 24 17:55:32 2010 +0200
@@ -540,18 +540,18 @@
 \isanewline
 \ \ structure\ Terms\ {\isacharequal}\ Theory{\isacharunderscore}Data\isanewline
 \ \ {\isacharparenleft}\isanewline
-\ \ \ \ type\ T\ {\isacharequal}\ term\ OrdList{\isachardot}T{\isacharsemicolon}\isanewline
+\ \ \ \ type\ T\ {\isacharequal}\ term\ Ord{\isacharunderscore}List{\isachardot}T{\isacharsemicolon}\isanewline
 \ \ \ \ val\ empty\ {\isacharequal}\ {\isacharbrackleft}{\isacharbrackright}{\isacharsemicolon}\isanewline
 \ \ \ \ val\ extend\ {\isacharequal}\ I{\isacharsemicolon}\isanewline
 \ \ \ \ fun\ merge\ {\isacharparenleft}ts{\isadigit{1}}{\isacharcomma}\ ts{\isadigit{2}}{\isacharparenright}\ {\isacharequal}\isanewline
-\ \ \ \ \ \ OrdList{\isachardot}union\ Term{\isacharunderscore}Ord{\isachardot}fast{\isacharunderscore}term{\isacharunderscore}ord\ ts{\isadigit{1}}\ ts{\isadigit{2}}{\isacharsemicolon}\isanewline
+\ \ \ \ \ \ Ord{\isacharunderscore}List{\isachardot}union\ Term{\isacharunderscore}Ord{\isachardot}fast{\isacharunderscore}term{\isacharunderscore}ord\ ts{\isadigit{1}}\ ts{\isadigit{2}}{\isacharsemicolon}\isanewline
 \ \ {\isacharparenright}\isanewline
 \isanewline
 \ \ val\ get\ {\isacharequal}\ Terms{\isachardot}get{\isacharsemicolon}\isanewline
 \isanewline
 \ \ fun\ add\ raw{\isacharunderscore}t\ thy\ {\isacharequal}\isanewline
 \ \ \ \ let\ val\ t\ {\isacharequal}\ Sign{\isachardot}cert{\isacharunderscore}term\ thy\ raw{\isacharunderscore}t\isanewline
-\ \ \ \ in\ Terms{\isachardot}map\ {\isacharparenleft}OrdList{\isachardot}insert\ Term{\isacharunderscore}Ord{\isachardot}fast{\isacharunderscore}term{\isacharunderscore}ord\ t{\isacharparenright}\ thy\ end{\isacharsemicolon}\isanewline
+\ \ \ \ in\ Terms{\isachardot}map\ {\isacharparenleft}Ord{\isacharunderscore}List{\isachardot}insert\ Term{\isacharunderscore}Ord{\isachardot}fast{\isacharunderscore}term{\isacharunderscore}ord\ t{\isacharparenright}\ thy\ end{\isacharsemicolon}\isanewline
 \isanewline
 \ \ end{\isacharsemicolon}\isanewline
 {\isacharverbatimclose}%
@@ -563,14 +563,14 @@
 \endisadelimML
 %
 \begin{isamarkuptext}%
-We use \verb|term OrdList.T| for reasonably efficient
+We use \verb|term Ord_List.T| for reasonably efficient
   representation of a set of terms: all operations are linear in the
   number of stored elements.  Here we assume that our users do not
   care about the declaration order, since that data structure forces
   its own arrangement of elements.
 
   Observe how the \verb|merge| operation joins the data slots of
-  the two constituents: \verb|OrdList.union| prevents duplication of
+  the two constituents: \verb|Ord_List.union| prevents duplication of
   common data from different branches, thus avoiding the danger of
   exponential blowup.  (Plain list append etc.\ must never be used for
   theory data merges.)
diff -r e75b993c0433 -r 1906c0c77341 doc-src/IsarRef/Thy/Document_Preparation.thy
--- a/doc-src/IsarRef/Thy/Document_Preparation.thy	Fri Sep 24 15:53:57 2010 +0200
+++ b/doc-src/IsarRef/Thy/Document_Preparation.thy	Fri Sep 24 17:55:32 2010 +0200
@@ -250,8 +250,8 @@
 
   \item @{text "@{typ \<tau>}"} prints a well-formed type @{text "\<tau>"}.
 
-  \item @{text "@{type \<kappa>}"} prints a type constructor
-    (logical or abbreviation) @{text "\<kappa>"}.
+  \item @{text "@{type \<kappa>}"} prints a (logical or syntactic) type
+    constructor @{text "\<kappa>"}.
 
   \item @{text "@{class c}"} prints a class @{text c}.
 
diff -r e75b993c0433 -r 1906c0c77341 doc-src/IsarRef/Thy/document/Document_Preparation.tex
--- a/doc-src/IsarRef/Thy/document/Document_Preparation.tex	Fri Sep 24 15:53:57 2010 +0200
+++ b/doc-src/IsarRef/Thy/document/Document_Preparation.tex	Fri Sep 24 17:55:32 2010 +0200
@@ -266,8 +266,8 @@
 
   \item \isa{{\isachardoublequote}{\isacharat}{\isacharbraceleft}typ\ {\isasymtau}{\isacharbraceright}{\isachardoublequote}} prints a well-formed type \isa{{\isachardoublequote}{\isasymtau}{\isachardoublequote}}.
 
-  \item \isa{{\isachardoublequote}{\isacharat}{\isacharbraceleft}type\ {\isasymkappa}{\isacharbraceright}{\isachardoublequote}} prints a type constructor
-    (logical or abbreviation) \isa{{\isachardoublequote}{\isasymkappa}{\isachardoublequote}}.
+  \item \isa{{\isachardoublequote}{\isacharat}{\isacharbraceleft}type\ {\isasymkappa}{\isacharbraceright}{\isachardoublequote}} prints a (logical or syntactic) type
+    constructor \isa{{\isachardoublequote}{\isasymkappa}{\isachardoublequote}}.
 
   \item \isa{{\isachardoublequote}{\isacharat}{\isacharbraceleft}class\ c{\isacharbraceright}{\isachardoublequote}} prints a class \isa{c}.
 
diff -r e75b993c0433 -r 1906c0c77341 src/HOL/Boogie/Tools/boogie_vcs.ML
--- a/src/HOL/Boogie/Tools/boogie_vcs.ML	Fri Sep 24 15:53:57 2010 +0200
+++ b/src/HOL/Boogie/Tools/boogie_vcs.ML	Fri Sep 24 17:55:32 2010 +0200
@@ -275,14 +275,14 @@
 
 structure Filters = Theory_Data
 (
-  type T = (serial * (term -> bool)) OrdList.T
+  type T = (serial * (term -> bool)) Ord_List.T
   val empty = []
   val extend = I
-  fun merge (fs1, fs2) = fold (OrdList.insert serial_ord) fs2 fs1
+  fun merge (fs1, fs2) = fold (Ord_List.insert serial_ord) fs2 fs1
 )
 
 fun add_assertion_filter f =
-  Filters.map (OrdList.insert serial_ord (serial (), f))
+  Filters.map (Ord_List.insert serial_ord (serial (), f))
 
 fun filter_assertions thy =
   let
diff -r e75b993c0433 -r 1906c0c77341 src/HOL/Matrix/Compute_Oracle/linker.ML
--- a/src/HOL/Matrix/Compute_Oracle/linker.ML	Fri Sep 24 15:53:57 2010 +0200
+++ b/src/HOL/Matrix/Compute_Oracle/linker.ML	Fri Sep 24 17:55:32 2010 +0200
@@ -166,7 +166,7 @@
                               else case Consttab.lookup insttab constant of
                                        SOME _ => instantiations
                                      | NONE => ((constant', (constant, Sign.typ_match thy (ty', ty) empty_subst))::instantiations
-                                                handle TYPE_MATCH => instantiations))
+                                                handle Type.TYPE_MATCH => instantiations))
                           ctab instantiations
         val instantiations = fold calc_instantiations cs []
         (*val _ = writeln ("instantiations = "^(makestring (length instantiations)))*)
diff -r e75b993c0433 -r 1906c0c77341 src/HOL/Tools/Nitpick/nitpick_hol.ML
--- a/src/HOL/Tools/Nitpick/nitpick_hol.ML	Fri Sep 24 15:53:57 2010 +0200
+++ b/src/HOL/Tools/Nitpick/nitpick_hol.ML	Fri Sep 24 17:55:32 2010 +0200
@@ -1254,9 +1254,9 @@
 fun partition_axioms_by_definitionality ctxt axioms def_names =
   let
     val axioms = sort (fast_string_ord o pairself fst) axioms
-    val defs = OrdList.inter (fast_string_ord o apsnd fst) def_names axioms
+    val defs = Ord_List.inter (fast_string_ord o apsnd fst) def_names axioms
     val nondefs =
-      OrdList.subtract (fast_string_ord o apsnd fst) def_names axioms
+      Ord_List.subtract (fast_string_ord o apsnd fst) def_names axioms
       |> filter_out ((is_arity_type_axiom orf is_typedef_axiom ctxt true) o snd)
   in pairself (map snd) (defs, nondefs) end
 
@@ -1289,7 +1289,7 @@
       #> filter_out (is_class_axiom o snd)
     val specs = Defs.all_specifications_of (Theory.defs_of thy)
     val def_names = specs |> maps snd |> map_filter #def
-                    |> OrdList.make fast_string_ord
+                    |> Ord_List.make fast_string_ord
     val thys = thy :: Theory.ancestors_of thy
     val (built_in_thys, user_thys) = List.partition is_built_in_theory thys
     val built_in_axioms = axioms_of_thys built_in_thys
diff -r e75b993c0433 -r 1906c0c77341 src/HOL/Tools/Nitpick/nitpick_preproc.ML
--- a/src/HOL/Tools/Nitpick/nitpick_preproc.ML	Fri Sep 24 15:53:57 2010 +0200
+++ b/src/HOL/Tools/Nitpick/nitpick_preproc.ML	Fri Sep 24 17:55:32 2010 +0200
@@ -687,7 +687,7 @@
       | call_sets [] uss vs = vs :: call_sets uss [] []
       | call_sets ([] :: _) _ _ = []
       | call_sets ((t :: ts) :: tss) uss vs =
-        OrdList.insert Term_Ord.term_ord t vs |> call_sets tss (ts :: uss)
+        Ord_List.insert Term_Ord.term_ord t vs |> call_sets tss (ts :: uss)
     val sets = call_sets (fun_calls t [] []) [] []
     val indexed_sets = sets ~~ (index_seq 0 (length sets))
   in
@@ -701,7 +701,7 @@
   end
 fun static_args_in_terms hol_ctxt x =
   map (static_args_in_term hol_ctxt x)
-  #> fold1 (OrdList.inter (prod_ord int_ord (option_ord Term_Ord.term_ord)))
+  #> fold1 (Ord_List.inter (prod_ord int_ord (option_ord Term_Ord.term_ord)))
 
 fun overlapping_indices [] _ = []
   | overlapping_indices _ [] = []
@@ -844,7 +844,7 @@
     fun generality (js, _, _) = ~(length js)
     fun is_more_specific (j1, t1, x1) (j2, t2, x2) =
       x1 <> x2 andalso length j2 < length j1 andalso
-      OrdList.subset (prod_ord int_ord Term_Ord.term_ord) (j2 ~~ t2, j1 ~~ t1)
+      Ord_List.subset (prod_ord int_ord Term_Ord.term_ord) (j2 ~~ t2, j1 ~~ t1)
     fun do_pass_1 _ [] [_] [_] = I
       | do_pass_1 T skipped _ [] = do_pass_2 T skipped
       | do_pass_1 T skipped all (z :: zs) =
diff -r e75b993c0433 -r 1906c0c77341 src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML
--- a/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML	Fri Sep 24 15:53:57 2010 +0200
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML	Fri Sep 24 17:55:32 2010 +0200
@@ -491,7 +491,7 @@
       fun subst_of (pred', pred) =
         let
           val subst = Sign.typ_match thy (fastype_of pred', fastype_of pred) Vartab.empty
-            handle TYPE_MATCH => error ("Type mismatch of predicate " ^ fst (dest_Const pred)
+            handle Type.TYPE_MATCH => error ("Type mismatch of predicate " ^ fst (dest_Const pred)
             ^ " (trying to match " ^ Syntax.string_of_typ ctxt (fastype_of pred')
             ^ " and " ^ Syntax.string_of_typ ctxt (fastype_of pred) ^ ")"
             ^ " in " ^ Display.string_of_thm ctxt th)
diff -r e75b993c0433 -r 1906c0c77341 src/HOL/Tools/SMT/smt_monomorph.ML
--- a/src/HOL/Tools/SMT/smt_monomorph.ML	Fri Sep 24 15:53:57 2010 +0200
+++ b/src/HOL/Tools/SMT/smt_monomorph.ML	Fri Sep 24 17:55:32 2010 +0200
@@ -29,7 +29,7 @@
 fun add_consts f =
   collect_consts_if f (fn (n, T) => Symtab.map_entry n (insert (op =) T))
 
-val insert_const = OrdList.insert (prod_ord fast_string_ord Term_Ord.typ_ord)
+val insert_const = Ord_List.insert (prod_ord fast_string_ord Term_Ord.typ_ord)
 fun tvar_consts_of thm = collect_consts_if typ_has_tvars insert_const thm []
 
 
diff -r e75b993c0433 -r 1906c0c77341 src/HOL/Tools/SMT/smtlib_interface.ML
--- a/src/HOL/Tools/SMT/smtlib_interface.ML	Fri Sep 24 15:53:57 2010 +0200
+++ b/src/HOL/Tools/SMT/smtlib_interface.ML	Fri Sep 24 17:55:32 2010 +0200
@@ -136,10 +136,10 @@
   type T = (int * builtins) list
   val empty = []
   val extend = I
-  fun merge (bs1, bs2) = OrdList.union fst_int_ord bs2 bs1
+  fun merge (bs1, bs2) = Ord_List.union fst_int_ord bs2 bs1
 )
 
-fun add_builtins bs = Builtins.map (OrdList.insert fst_int_ord (serial (), bs))
+fun add_builtins bs = Builtins.map (Ord_List.insert fst_int_ord (serial (), bs))
 
 fun get_builtins ctxt = map snd (Builtins.get (Context.Proof ctxt))
 
@@ -212,10 +212,10 @@
   type T = (int * (term list -> string option)) list
   val empty = []
   val extend = I
-  fun merge (bs1, bs2) = OrdList.union fst_int_ord bs2 bs1
+  fun merge (bs1, bs2) = Ord_List.union fst_int_ord bs2 bs1
 )
 
-fun add_logic l = Logics.map (OrdList.insert fst_int_ord (serial (), l))
+fun add_logic l = Logics.map (Ord_List.insert fst_int_ord (serial (), l))
 
 fun choose_logic ctxt ts =
   let
diff -r e75b993c0433 -r 1906c0c77341 src/HOL/Tools/SMT/z3_interface.ML
--- a/src/HOL/Tools/SMT/z3_interface.ML	Fri Sep 24 15:53:57 2010 +0200
+++ b/src/HOL/Tools/SMT/z3_interface.ML	Fri Sep 24 17:55:32 2010 +0200
@@ -43,11 +43,11 @@
   type T = (int * builtin_fun) list
   val empty = []
   val extend = I
-  fun merge (bs1, bs2) = OrdList.union fst_int_ord bs2 bs1
+  fun merge (bs1, bs2) = Ord_List.union fst_int_ord bs2 bs1
 )
 
 fun add_builtin_funs b =
-  Builtins.map (OrdList.insert fst_int_ord (serial (), b))
+  Builtins.map (Ord_List.insert fst_int_ord (serial (), b))
 
 fun get_builtin_funs ctxt c ts =
   let
@@ -143,11 +143,11 @@
   type T = (int * mk_builtins) list
   val empty = []
   val extend = I
-  fun merge (bs1, bs2) = OrdList.union fst_int_ord bs2 bs1
+  fun merge (bs1, bs2) = Ord_List.union fst_int_ord bs2 bs1
 )
 
 fun add_mk_builtins mk =
-  Mk_Builtins.map (OrdList.insert fst_int_ord (serial (), mk))
+  Mk_Builtins.map (Ord_List.insert fst_int_ord (serial (), mk))
 
 fun get_mk_builtins ctxt = map snd (Mk_Builtins.get (Context.Proof ctxt))
 
diff -r e75b993c0433 -r 1906c0c77341 src/HOL/Tools/sat_solver.ML
--- a/src/HOL/Tools/sat_solver.ML	Fri Sep 24 15:53:57 2010 +0200
+++ b/src/HOL/Tools/sat_solver.ML	Fri Sep 24 17:55:32 2010 +0200
@@ -600,7 +600,7 @@
       (* representation of clauses as ordered lists of literals (with duplicates removed) *)
       (* prop_formula -> int list *)
       fun clause_to_lit_list (PropLogic.Or (fm1, fm2)) =
-        OrdList.union int_ord (clause_to_lit_list fm1) (clause_to_lit_list fm2)
+        Ord_List.union int_ord (clause_to_lit_list fm1) (clause_to_lit_list fm2)
         | clause_to_lit_list (PropLogic.BoolVar i) =
         [i]
         | clause_to_lit_list (PropLogic.Not (PropLogic.BoolVar i)) =
diff -r e75b993c0433 -r 1906c0c77341 src/Pure/General/ord_list.ML
--- a/src/Pure/General/ord_list.ML	Fri Sep 24 15:53:57 2010 +0200
+++ b/src/Pure/General/ord_list.ML	Fri Sep 24 17:55:32 2010 +0200
@@ -18,7 +18,7 @@
   val subtract: ('b * 'a -> order) -> 'b T -> 'a T -> 'a T
 end;
 
-structure OrdList: ORD_LIST =
+structure Ord_List: ORD_LIST =
 struct
 
 type 'a T = 'a list;
diff -r e75b993c0433 -r 1906c0c77341 src/Pure/Thy/thy_output.ML
--- a/src/Pure/Thy/thy_output.ML	Fri Sep 24 15:53:57 2010 +0200
+++ b/src/Pure/Thy/thy_output.ML	Fri Sep 24 17:55:32 2010 +0200
@@ -511,10 +511,8 @@
   Pretty.str o Type.extern_class (ProofContext.tsig_of ctxt) o ProofContext.read_class ctxt;
 
 fun pretty_type ctxt s =
-  let
-    val tsig = ProofContext.tsig_of ctxt;
-    val _ = ProofContext.read_type_name ctxt false s;
-  in (Pretty.str o Type.extern_type tsig o Type.intern_type tsig) s end;
+  let val Type (name, _) = ProofContext.read_type_name_proper ctxt false s
+  in Pretty.str (Type.extern_type (ProofContext.tsig_of ctxt) name) end;
 
 fun pretty_prf full ctxt = Proof_Syntax.pretty_proof_of ctxt full;
 
diff -r e75b993c0433 -r 1906c0c77341 src/Pure/old_term.ML
--- a/src/Pure/old_term.ML	Fri Sep 24 15:53:57 2010 +0200
+++ b/src/Pure/old_term.ML	Fri Sep 24 17:55:32 2010 +0200
@@ -75,7 +75,7 @@
 
 (*Accumulates the Vars in the term, suppressing duplicates.*)
 fun add_term_vars (t, vars: term list) = case t of
-    Var   _ => OrdList.insert Term_Ord.term_ord t vars
+    Var   _ => Ord_List.insert Term_Ord.term_ord t vars
   | Abs (_,_,body) => add_term_vars(body,vars)
   | f$t =>  add_term_vars (f, add_term_vars(t, vars))
   | _ => vars;
@@ -84,7 +84,7 @@
 
 (*Accumulates the Frees in the term, suppressing duplicates.*)
 fun add_term_frees (t, frees: term list) = case t of
-    Free   _ => OrdList.insert Term_Ord.term_ord t frees
+    Free   _ => Ord_List.insert Term_Ord.term_ord t frees
   | Abs (_,_,body) => add_term_frees(body,frees)
   | f$t =>  add_term_frees (f, add_term_frees(t, frees))
   | _ => frees;
diff -r e75b993c0433 -r 1906c0c77341 src/Pure/proofterm.ML
--- a/src/Pure/proofterm.ML	Fri Sep 24 15:53:57 2010 +0200
+++ b/src/Pure/proofterm.ML	Fri Sep 24 17:55:32 2010 +0200
@@ -24,8 +24,8 @@
    | Promise of serial * term * typ list
    | PThm of serial * ((string * term * typ list option) * proof_body future)
   and proof_body = PBody of
-    {oracles: (string * term) OrdList.T,
-     thms: (serial * (string * term * proof_body future)) OrdList.T,
+    {oracles: (string * term) Ord_List.T,
+     thms: (serial * (string * term * proof_body future)) Ord_List.T,
      proof: proof}
 
   val %> : proof * term -> proof
@@ -46,9 +46,9 @@
 
   val oracle_ord: oracle * oracle -> order
   val thm_ord: pthm * pthm -> order
-  val merge_oracles: oracle OrdList.T -> oracle OrdList.T -> oracle OrdList.T
-  val merge_thms: pthm OrdList.T -> pthm OrdList.T -> pthm OrdList.T
-  val all_oracles_of: proof_body -> oracle OrdList.T
+  val merge_oracles: oracle Ord_List.T -> oracle Ord_List.T -> oracle Ord_List.T
+  val merge_thms: pthm Ord_List.T -> pthm Ord_List.T -> pthm Ord_List.T
+  val all_oracles_of: proof_body -> oracle Ord_List.T
   val approximate_proof_body: proof -> proof_body
 
   (** primitive operations **)
@@ -163,8 +163,8 @@
  | Promise of serial * term * typ list
  | PThm of serial * ((string * term * typ list option) * proof_body future)
 and proof_body = PBody of
-  {oracles: (string * term) OrdList.T,
-   thms: (serial * (string * term * proof_body future)) OrdList.T,
+  {oracles: (string * term) Ord_List.T,
+   thms: (serial * (string * term * proof_body future)) Ord_List.T,
    proof: proof};
 
 type oracle = string * term;
@@ -235,8 +235,8 @@
 val oracle_ord = prod_ord fast_string_ord Term_Ord.fast_term_ord;
 fun thm_ord ((i, _): pthm, (j, _)) = int_ord (j, i);
 
-val merge_oracles = OrdList.union oracle_ord;
-val merge_thms = OrdList.union thm_ord;
+val merge_oracles = Ord_List.union oracle_ord;
+val merge_thms = Ord_List.union thm_ord;
 
 val all_oracles_of =
   let
@@ -259,8 +259,8 @@
         | _ => I) [prf] ([], []);
   in
     PBody
-     {oracles = OrdList.make oracle_ord oracles,
-      thms = OrdList.make thm_ord thms,
+     {oracles = Ord_List.make oracle_ord oracles,
+      thms = Ord_List.make thm_ord thms,
       proof = prf}
   end;
 
diff -r e75b993c0433 -r 1906c0c77341 src/Pure/sorts.ML
--- a/src/Pure/sorts.ML	Fri Sep 24 15:53:57 2010 +0200
+++ b/src/Pure/sorts.ML	Fri Sep 24 17:55:32 2010 +0200
@@ -14,16 +14,16 @@
 
 signature SORTS =
 sig
-  val make: sort list -> sort OrdList.T
-  val subset: sort OrdList.T * sort OrdList.T -> bool
-  val union: sort OrdList.T -> sort OrdList.T -> sort OrdList.T
-  val subtract: sort OrdList.T -> sort OrdList.T -> sort OrdList.T
-  val remove_sort: sort -> sort OrdList.T -> sort OrdList.T
-  val insert_sort: sort -> sort OrdList.T -> sort OrdList.T
-  val insert_typ: typ -> sort OrdList.T -> sort OrdList.T
-  val insert_typs: typ list -> sort OrdList.T -> sort OrdList.T
-  val insert_term: term -> sort OrdList.T -> sort OrdList.T
-  val insert_terms: term list -> sort OrdList.T -> sort OrdList.T
+  val make: sort list -> sort Ord_List.T
+  val subset: sort Ord_List.T * sort Ord_List.T -> bool
+  val union: sort Ord_List.T -> sort Ord_List.T -> sort Ord_List.T
+  val subtract: sort Ord_List.T -> sort Ord_List.T -> sort Ord_List.T
+  val remove_sort: sort -> sort Ord_List.T -> sort Ord_List.T
+  val insert_sort: sort -> sort Ord_List.T -> sort Ord_List.T
+  val insert_typ: typ -> sort Ord_List.T -> sort Ord_List.T
+  val insert_typs: typ list -> sort Ord_List.T -> sort Ord_List.T
+  val insert_term: term -> sort Ord_List.T -> sort Ord_List.T
+  val insert_terms: term list -> sort Ord_List.T -> sort Ord_List.T
   type algebra
   val classes_of: algebra -> serial Graph.T
   val arities_of: algebra -> (class * sort list) list Symtab.table
@@ -37,7 +37,7 @@
   val inter_sort: algebra -> sort * sort -> sort
   val minimize_sort: algebra -> sort -> sort
   val complete_sort: algebra -> sort -> sort
-  val minimal_sorts: algebra -> sort list -> sort OrdList.T
+  val minimal_sorts: algebra -> sort list -> sort Ord_List.T
   val certify_class: algebra -> class -> class    (*exception TYPE*)
   val certify_sort: algebra -> sort -> sort       (*exception TYPE*)
   val add_class: Pretty.pp -> class * class list -> algebra -> algebra
@@ -71,13 +71,13 @@
 
 (** ordered lists of sorts **)
 
-val make = OrdList.make Term_Ord.sort_ord;
-val subset = OrdList.subset Term_Ord.sort_ord;
-val union = OrdList.union Term_Ord.sort_ord;
-val subtract = OrdList.subtract Term_Ord.sort_ord;
+val make = Ord_List.make Term_Ord.sort_ord;
+val subset = Ord_List.subset Term_Ord.sort_ord;
+val union = Ord_List.union Term_Ord.sort_ord;
+val subtract = Ord_List.subtract Term_Ord.sort_ord;
 
-val remove_sort = OrdList.remove Term_Ord.sort_ord;
-val insert_sort = OrdList.insert Term_Ord.sort_ord;
+val remove_sort = Ord_List.remove Term_Ord.sort_ord;
+val insert_sort = Ord_List.insert Term_Ord.sort_ord;
 
 fun insert_typ (TFree (_, S)) Ss = insert_sort S Ss
   | insert_typ (TVar (_, S)) Ss = insert_sort S Ss
diff -r e75b993c0433 -r 1906c0c77341 src/Pure/thm.ML
--- a/src/Pure/thm.ML	Fri Sep 24 15:53:57 2010 +0200
+++ b/src/Pure/thm.ML	Fri Sep 24 17:55:32 2010 +0200
@@ -15,7 +15,7 @@
    {thy_ref: theory_ref,
     T: typ,
     maxidx: int,
-    sorts: sort OrdList.T}
+    sorts: sort Ord_List.T}
   val theory_of_ctyp: ctyp -> theory
   val typ_of: ctyp -> typ
   val ctyp_of: theory -> typ -> ctyp
@@ -28,9 +28,9 @@
     t: term,
     T: typ,
     maxidx: int,
-    sorts: sort OrdList.T}
+    sorts: sort Ord_List.T}
   val crep_cterm: cterm ->
-    {thy_ref: theory_ref, t: term, T: ctyp, maxidx: int, sorts: sort OrdList.T}
+    {thy_ref: theory_ref, t: term, T: ctyp, maxidx: int, sorts: sort Ord_List.T}
   val theory_of_cterm: cterm -> theory
   val term_of: cterm -> term
   val cterm_of: theory -> term -> cterm
@@ -44,16 +44,16 @@
    {thy_ref: theory_ref,
     tags: Properties.T,
     maxidx: int,
-    shyps: sort OrdList.T,
-    hyps: term OrdList.T,
+    shyps: sort Ord_List.T,
+    hyps: term Ord_List.T,
     tpairs: (term * term) list,
     prop: term}
   val crep_thm: thm ->
    {thy_ref: theory_ref,
     tags: Properties.T,
     maxidx: int,
-    shyps: sort OrdList.T,
-    hyps: cterm OrdList.T,
+    shyps: sort Ord_List.T,
+    hyps: cterm Ord_List.T,
     tpairs: (cterm * cterm) list,
     prop: cterm}
   exception THM of string * int * thm list
@@ -163,7 +163,7 @@
  {thy_ref: theory_ref,
   T: typ,
   maxidx: int,
-  sorts: sort OrdList.T}
+  sorts: sort Ord_List.T}
 with
 
 fun rep_ctyp (Ctyp args) = args;
@@ -191,7 +191,7 @@
   t: term,
   T: typ,
   maxidx: int,
-  sorts: sort OrdList.T}
+  sorts: sort Ord_List.T}
 with
 
 exception CTERM of string * cterm list;
@@ -339,12 +339,12 @@
  {thy_ref: theory_ref,                          (*dynamic reference to theory*)
   tags: Properties.T,                           (*additional annotations/comments*)
   maxidx: int,                                  (*maximum index of any Var or TVar*)
-  shyps: sort OrdList.T,                        (*sort hypotheses*)
-  hyps: term OrdList.T,                         (*hypotheses*)
+  shyps: sort Ord_List.T,                        (*sort hypotheses*)
+  hyps: term Ord_List.T,                         (*hypotheses*)
   tpairs: (term * term) list,                   (*flex-flex pairs*)
   prop: term}                                   (*conclusion*)
 and deriv = Deriv of
- {promises: (serial * thm future) OrdList.T,
+ {promises: (serial * thm future) Ord_List.T,
   body: Proofterm.proof_body}
 with
 
@@ -380,9 +380,9 @@
 
 fun full_prop_of (Thm (_, {tpairs, prop, ...})) = attach_tpairs tpairs prop;
 
-val union_hyps = OrdList.union Term_Ord.fast_term_ord;
-val insert_hyps = OrdList.insert Term_Ord.fast_term_ord;
-val remove_hyps = OrdList.remove Term_Ord.fast_term_ord;
+val union_hyps = Ord_List.union Term_Ord.fast_term_ord;
+val insert_hyps = Ord_List.insert Term_Ord.fast_term_ord;
+val remove_hyps = Ord_List.remove Term_Ord.fast_term_ord;
 
 
 (* merge theories of cterms/thms -- trivial absorption only *)
@@ -493,7 +493,7 @@
     (Deriv {promises = ps1, body = PBody {oracles = oras1, thms = thms1, proof = prf1}})
     (Deriv {promises = ps2, body = PBody {oracles = oras2, thms = thms2, proof = prf2}}) =
   let
-    val ps = OrdList.union promise_ord ps1 ps2;
+    val ps = Ord_List.union promise_ord ps1 ps2;
     val oras = Proofterm.merge_oracles oras1 oras2;
     val thms = Proofterm.merge_thms thms1 thms2;
     val prf =
diff -r e75b993c0433 -r 1906c0c77341 src/Pure/variable.ML
--- a/src/Pure/variable.ML	Fri Sep 24 15:53:57 2010 +0200
+++ b/src/Pure/variable.ML	Fri Sep 24 17:55:32 2010 +0200
@@ -77,7 +77,7 @@
   binds: (typ * term) Vartab.table,     (*term bindings*)
   type_occs: string list Symtab.table,  (*type variables -- possibly within term variables*)
   maxidx: int,                          (*maximum var index*)
-  sorts: sort OrdList.T,                (*declared sort occurrences*)
+  sorts: sort Ord_List.T,                (*declared sort occurrences*)
   constraints:
     typ Vartab.table *                  (*type constraints*)
     sort Vartab.table};                 (*default sorts*)
diff -r e75b993c0433 -r 1906c0c77341 src/Tools/jEdit/src/jedit/document_view.scala
--- a/src/Tools/jEdit/src/jedit/document_view.scala	Fri Sep 24 15:53:57 2010 +0200
+++ b/src/Tools/jEdit/src/jedit/document_view.scala	Fri Sep 24 17:55:32 2010 +0200
@@ -230,14 +230,14 @@
               case _ =>
             }
 
-            // boxed text
+            // background boxes
             for {
               Text.Info(range, Some(color)) <-
                 snapshot.select_markup(line_range)(Isabelle_Markup.box).iterator
               r <- Isabelle.gfx_range(text_area, range)
             } {
               gfx.setColor(color)
-              gfx.drawRect(r.x + 1, y + i * line_height + 1, r.length - 2, line_height - 3)
+              gfx.fillRect(r.x + 1, y + i * line_height + 1, r.length - 2, line_height - 2)
             }
 
             // squiggly underline
diff -r e75b993c0433 -r 1906c0c77341 src/Tools/jEdit/src/jedit/isabelle_markup.scala
--- a/src/Tools/jEdit/src/jedit/isabelle_markup.scala	Fri Sep 24 15:53:57 2010 +0200
+++ b/src/Tools/jEdit/src/jedit/isabelle_markup.scala	Fri Sep 24 17:55:32 2010 +0200
@@ -21,10 +21,11 @@
   val outdated_color = new Color(240, 240, 240)
   val unfinished_color = new Color(255, 228, 225)
 
+  val light_color = new Color(240, 240, 240)
   val regular_color = new Color(192, 192, 192)
-  val warning_color = new Color(255, 168, 0)
-  val error_color = new Color(255, 80, 80)
-  val bad_color = new Color(255, 204, 153, 100)
+  val warning_color = new Color(255, 140, 0)
+  val error_color = new Color(178, 34, 34)
+  val bad_color = new Color(255, 106, 106, 100)
 
   class Icon(val priority: Int, val icon: javax.swing.Icon)
   {
@@ -96,7 +97,7 @@
 
   val box: Markup_Tree.Select[Color] =
   {
-    case Text.Info(_, XML.Elem(Markup(Markup.TOKEN_RANGE, _), _)) => regular_color
+    case Text.Info(_, XML.Elem(Markup(Markup.TOKEN_RANGE, _), _)) => light_color
   }
 
   val tooltip: Markup_Tree.Select[String] =