# HG changeset patch
# User haftmann
# Date 1285570043 -7200
# Node ID d3f46f1ca1f1adae0bf0850c03695e9897a10987
# Parent  6542245db5c2961b0a71f8fb41d716be84bd73b6# Parent  94b1890e4e4a0be38d7dffb8654bb92e44ba9779
merged

diff -r 94b1890e4e4a -r d3f46f1ca1f1 Admin/isatest/isatest-makeall
--- a/Admin/isatest/isatest-makeall	Mon Sep 27 08:46:53 2010 +0200
+++ b/Admin/isatest/isatest-makeall	Mon Sep 27 08:47:23 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 94b1890e4e4a -r d3f46f1ca1f1 NEWS
--- a/NEWS	Mon Sep 27 08:46:53 2010 +0200
+++ b/NEWS	Mon Sep 27 08:47:23 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 94b1890e4e4a -r d3f46f1ca1f1 doc-src/IsarImplementation/Thy/Prelim.thy
--- a/doc-src/IsarImplementation/Thy/Prelim.thy	Mon Sep 27 08:46:53 2010 +0200
+++ b/doc-src/IsarImplementation/Thy/Prelim.thy	Mon Sep 27 08:47:23 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 94b1890e4e4a -r d3f46f1ca1f1 doc-src/IsarImplementation/Thy/document/Prelim.tex
--- a/doc-src/IsarImplementation/Thy/document/Prelim.tex	Mon Sep 27 08:46:53 2010 +0200
+++ b/doc-src/IsarImplementation/Thy/document/Prelim.tex	Mon Sep 27 08:47:23 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 94b1890e4e4a -r d3f46f1ca1f1 doc-src/IsarRef/Thy/Document_Preparation.thy
--- a/doc-src/IsarRef/Thy/Document_Preparation.thy	Mon Sep 27 08:46:53 2010 +0200
+++ b/doc-src/IsarRef/Thy/Document_Preparation.thy	Mon Sep 27 08:47:23 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 94b1890e4e4a -r d3f46f1ca1f1 doc-src/IsarRef/Thy/document/Document_Preparation.tex
--- a/doc-src/IsarRef/Thy/document/Document_Preparation.tex	Mon Sep 27 08:46:53 2010 +0200
+++ b/doc-src/IsarRef/Thy/document/Document_Preparation.tex	Mon Sep 27 08:47:23 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 94b1890e4e4a -r d3f46f1ca1f1 src/HOL/Boogie/Tools/boogie_vcs.ML
--- a/src/HOL/Boogie/Tools/boogie_vcs.ML	Mon Sep 27 08:46:53 2010 +0200
+++ b/src/HOL/Boogie/Tools/boogie_vcs.ML	Mon Sep 27 08:47:23 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 94b1890e4e4a -r d3f46f1ca1f1 src/HOL/Matrix/Compute_Oracle/linker.ML
--- a/src/HOL/Matrix/Compute_Oracle/linker.ML	Mon Sep 27 08:46:53 2010 +0200
+++ b/src/HOL/Matrix/Compute_Oracle/linker.ML	Mon Sep 27 08:47:23 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 94b1890e4e4a -r d3f46f1ca1f1 src/HOL/Tools/Nitpick/nitpick_hol.ML
--- a/src/HOL/Tools/Nitpick/nitpick_hol.ML	Mon Sep 27 08:46:53 2010 +0200
+++ b/src/HOL/Tools/Nitpick/nitpick_hol.ML	Mon Sep 27 08:47:23 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 94b1890e4e4a -r d3f46f1ca1f1 src/HOL/Tools/Nitpick/nitpick_preproc.ML
--- a/src/HOL/Tools/Nitpick/nitpick_preproc.ML	Mon Sep 27 08:46:53 2010 +0200
+++ b/src/HOL/Tools/Nitpick/nitpick_preproc.ML	Mon Sep 27 08:47:23 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 94b1890e4e4a -r d3f46f1ca1f1 src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML
--- a/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML	Mon Sep 27 08:46:53 2010 +0200
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML	Mon Sep 27 08:47:23 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 94b1890e4e4a -r d3f46f1ca1f1 src/HOL/Tools/SMT/smt_monomorph.ML
--- a/src/HOL/Tools/SMT/smt_monomorph.ML	Mon Sep 27 08:46:53 2010 +0200
+++ b/src/HOL/Tools/SMT/smt_monomorph.ML	Mon Sep 27 08:47:23 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 94b1890e4e4a -r d3f46f1ca1f1 src/HOL/Tools/SMT/smtlib_interface.ML
--- a/src/HOL/Tools/SMT/smtlib_interface.ML	Mon Sep 27 08:46:53 2010 +0200
+++ b/src/HOL/Tools/SMT/smtlib_interface.ML	Mon Sep 27 08:47:23 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 94b1890e4e4a -r d3f46f1ca1f1 src/HOL/Tools/SMT/z3_interface.ML
--- a/src/HOL/Tools/SMT/z3_interface.ML	Mon Sep 27 08:46:53 2010 +0200
+++ b/src/HOL/Tools/SMT/z3_interface.ML	Mon Sep 27 08:47:23 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 94b1890e4e4a -r d3f46f1ca1f1 src/HOL/Tools/Sledgehammer/sledgehammer_reconstruct.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_reconstruct.ML	Mon Sep 27 08:46:53 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_reconstruct.ML	Mon Sep 27 08:47:23 2010 +0200
@@ -228,8 +228,8 @@
                       | NONE => ~1
   in if k >= 0 then [k] else [] end
 
-val is_axiom = not o null oo resolve_axiom
-val is_conjecture = not o null oo resolve_conjecture
+fun is_axiom conjecture_shape = not o null o resolve_axiom conjecture_shape
+fun is_conjecture conjecture_shape = not o null o resolve_conjecture conjecture_shape
 
 fun raw_label_for_name conjecture_shape name =
   case resolve_conjecture conjecture_shape name of
diff -r 94b1890e4e4a -r d3f46f1ca1f1 src/HOL/Tools/sat_solver.ML
--- a/src/HOL/Tools/sat_solver.ML	Mon Sep 27 08:46:53 2010 +0200
+++ b/src/HOL/Tools/sat_solver.ML	Mon Sep 27 08:47:23 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 94b1890e4e4a -r d3f46f1ca1f1 src/Pure/General/ord_list.ML
--- a/src/Pure/General/ord_list.ML	Mon Sep 27 08:46:53 2010 +0200
+++ b/src/Pure/General/ord_list.ML	Mon Sep 27 08:47:23 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 94b1890e4e4a -r d3f46f1ca1f1 src/Pure/Thy/thy_output.ML
--- a/src/Pure/Thy/thy_output.ML	Mon Sep 27 08:46:53 2010 +0200
+++ b/src/Pure/Thy/thy_output.ML	Mon Sep 27 08:47:23 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 94b1890e4e4a -r d3f46f1ca1f1 src/Pure/old_term.ML
--- a/src/Pure/old_term.ML	Mon Sep 27 08:46:53 2010 +0200
+++ b/src/Pure/old_term.ML	Mon Sep 27 08:47:23 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 94b1890e4e4a -r d3f46f1ca1f1 src/Pure/proofterm.ML
--- a/src/Pure/proofterm.ML	Mon Sep 27 08:46:53 2010 +0200
+++ b/src/Pure/proofterm.ML	Mon Sep 27 08:47:23 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 94b1890e4e4a -r d3f46f1ca1f1 src/Pure/sorts.ML
--- a/src/Pure/sorts.ML	Mon Sep 27 08:46:53 2010 +0200
+++ b/src/Pure/sorts.ML	Mon Sep 27 08:47:23 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 94b1890e4e4a -r d3f46f1ca1f1 src/Pure/thm.ML
--- a/src/Pure/thm.ML	Mon Sep 27 08:46:53 2010 +0200
+++ b/src/Pure/thm.ML	Mon Sep 27 08:47:23 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 94b1890e4e4a -r d3f46f1ca1f1 src/Pure/variable.ML
--- a/src/Pure/variable.ML	Mon Sep 27 08:46:53 2010 +0200
+++ b/src/Pure/variable.ML	Mon Sep 27 08:47:23 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 94b1890e4e4a -r d3f46f1ca1f1 src/Tools/jEdit/src/jedit/document_view.scala
--- a/src/Tools/jEdit/src/jedit/document_view.scala	Mon Sep 27 08:46:53 2010 +0200
+++ b/src/Tools/jEdit/src/jedit/document_view.scala	Mon Sep 27 08:47:23 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 94b1890e4e4a -r d3f46f1ca1f1 src/Tools/jEdit/src/jedit/isabelle_markup.scala
--- a/src/Tools/jEdit/src/jedit/isabelle_markup.scala	Mon Sep 27 08:46:53 2010 +0200
+++ b/src/Tools/jEdit/src/jedit/isabelle_markup.scala	Mon Sep 27 08:47:23 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] =