merged
authorblanchet
Mon, 20 Sep 2010 10:29:29 +0200
changeset 39549 346f6d79cba6
parent 39540 49c319fff40c (diff)
parent 39548 b96941dddd04 (current diff)
child 39550 f97fa74c388e
merged
--- a/doc-src/Classes/style.sty	Sat Sep 18 10:43:52 2010 +0200
+++ b/doc-src/Classes/style.sty	Mon Sep 20 10:29:29 2010 +0200
@@ -17,9 +17,6 @@
 %% typographic conventions
 \newcommand{\qt}[1]{``{#1}''}
 
-%% verbatim text
-\newcommand{\isatypewriter}{\fontsize{9pt}{0pt}\tt\renewcommand{\baselinestretch}{1}\setlength{\baselineskip}{9pt}}
-
 %% quote environment
 \isakeeptag{quote}
 \renewenvironment{quote}
--- a/doc-src/Codegen/style.sty	Sat Sep 18 10:43:52 2010 +0200
+++ b/doc-src/Codegen/style.sty	Mon Sep 20 10:29:29 2010 +0200
@@ -17,9 +17,6 @@
 \newcommand{\qt}[1]{``{#1}''}
 \newcommand{\ditem}[1]{\item[\isastyletext #1]}
 
-%% verbatim text
-\newcommand{\isatypewriter}{\fontsize{9pt}{0pt}\tt\renewcommand{\baselinestretch}{1}\setlength{\baselineskip}{9pt}}
-
 %% quote environment
 \isakeeptag{quote}
 \renewenvironment{quote}
--- a/doc-src/IsarRef/Thy/document/Document_Preparation.tex	Sat Sep 18 10:43:52 2010 +0200
+++ b/doc-src/IsarRef/Thy/document/Document_Preparation.tex	Mon Sep 20 10:29:29 2010 +0200
@@ -164,6 +164,8 @@
     \indexdef{}{antiquotation}{const}\hypertarget{antiquotation.const}{\hyperlink{antiquotation.const}{\mbox{\isa{const}}}} & : & \isa{antiquotation} \\
     \indexdef{}{antiquotation}{abbrev}\hypertarget{antiquotation.abbrev}{\hyperlink{antiquotation.abbrev}{\mbox{\isa{abbrev}}}} & : & \isa{antiquotation} \\
     \indexdef{}{antiquotation}{typ}\hypertarget{antiquotation.typ}{\hyperlink{antiquotation.typ}{\mbox{\isa{typ}}}} & : & \isa{antiquotation} \\
+    \indexdef{}{antiquotation}{type}\hypertarget{antiquotation.type}{\hyperlink{antiquotation.type}{\mbox{\isa{type}}}} & : & \isa{antiquotation} \\
+    \indexdef{}{antiquotation}{class}\hypertarget{antiquotation.class}{\hyperlink{antiquotation.class}{\mbox{\isa{class}}}} & : & \isa{antiquotation} \\
     \indexdef{}{antiquotation}{text}\hypertarget{antiquotation.text}{\hyperlink{antiquotation.text}{\mbox{\isa{text}}}} & : & \isa{antiquotation} \\
     \indexdef{}{antiquotation}{goals}\hypertarget{antiquotation.goals}{\hyperlink{antiquotation.goals}{\mbox{\isa{goals}}}} & : & \isa{antiquotation} \\
     \indexdef{}{antiquotation}{subgoals}\hypertarget{antiquotation.subgoals}{\hyperlink{antiquotation.subgoals}{\mbox{\isa{subgoals}}}} & : & \isa{antiquotation} \\
@@ -208,6 +210,8 @@
       'const' options term |
       'abbrev' options term |
       'typ' options type |
+      'type' options name |
+      'class' options name |
       'text' options name |
       'goals' options |
       'subgoals' options |
@@ -259,8 +263,14 @@
   
   \item \isa{{\isachardoublequote}{\isacharat}{\isacharbraceleft}abbrev\ c\ x\isactrlsub {\isadigit{1}}\ {\isasymdots}\ x\isactrlsub n{\isacharbraceright}{\isachardoublequote}} prints a constant abbreviation
   \isa{{\isachardoublequote}c\ x\isactrlsub {\isadigit{1}}\ {\isasymdots}\ x\isactrlsub n\ {\isasymequiv}\ rhs{\isachardoublequote}} as defined in the current context.
+
   \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}class\ c{\isacharbraceright}{\isachardoublequote}} prints a class \isa{c}.
+
   \item \isa{{\isachardoublequote}{\isacharat}{\isacharbraceleft}text\ s{\isacharbraceright}{\isachardoublequote}} prints uninterpreted source text \isa{s}.  This is particularly useful to print portions of text according
   to the Isabelle document style, without demanding well-formedness,
   e.g.\ small pieces of terms that should not be parsed or
--- a/doc-src/isabelle.sty	Sat Sep 18 10:43:52 2010 +0200
+++ b/doc-src/isabelle.sty	Mon Sep 20 10:29:29 2010 +0200
@@ -1,5 +1,3 @@
-%%
-%% 
 %%
 %% macros for Isabelle generated LaTeX output
 %%
@@ -48,6 +46,8 @@
 {\begin{trivlist}\begin{isabellebody}\item\relax}
 {\end{isabellebody}\end{trivlist}}
 
+\newcommand{\isatypewriter}{\fontsize{9pt}{0pt}\tt\renewcommand{\baselinestretch}{1}\setlength{\baselineskip}{9pt}}
+
 \newcommand{\isa}[1]{\emph{\isastyleminor #1}}
 
 \newcommand{\isaindent}[1]{\hphantom{#1}}
--- a/doc-src/more_antiquote.ML	Sat Sep 18 10:43:52 2010 +0200
+++ b/doc-src/more_antiquote.ML	Mon Sep 20 10:29:29 2010 +0200
@@ -29,7 +29,7 @@
   let
     val thy = ProofContext.theory_of ctxt;
     val const = Code.check_const thy raw_const;
-    val (_, eqngr) = Code_Preproc.obtain thy [const] [];
+    val (_, eqngr) = Code_Preproc.obtain true thy [const] [];
     fun holize thm = @{thm meta_eq_to_obj_eq} OF [thm];
     val thms = Code_Preproc.cert eqngr const
       |> Code.equations_of_cert thy
--- a/lib/texinputs/isabelle.sty	Sat Sep 18 10:43:52 2010 +0200
+++ b/lib/texinputs/isabelle.sty	Mon Sep 20 10:29:29 2010 +0200
@@ -46,6 +46,8 @@
 {\begin{trivlist}\begin{isabellebody}\item\relax}
 {\end{isabellebody}\end{trivlist}}
 
+\newcommand{\isatypewriter}{\fontsize{9pt}{0pt}\tt\renewcommand{\baselinestretch}{1}\setlength{\baselineskip}{9pt}}
+
 \newcommand{\isa}[1]{\emph{\isastyleminor #1}}
 
 \newcommand{\isaindent}[1]{\hphantom{#1}}
--- a/src/HOL/Library/Multiset.thy	Sat Sep 18 10:43:52 2010 +0200
+++ b/src/HOL/Library/Multiset.thy	Mon Sep 20 10:29:29 2010 +0200
@@ -779,8 +779,8 @@
   by (induct xs) (auto simp: add_ac)
 
 lemma count_filter:
-  "count (multiset_of xs) x = length [y \<leftarrow> xs. y = x]"
-by (induct xs) auto
+  "count (multiset_of xs) x = length (filter (\<lambda>y. x = y) xs)"
+  by (induct xs) auto
 
 lemma nth_mem_multiset_of: "i < length ls \<Longrightarrow> (ls ! i) :# multiset_of ls"
 apply (induct ls arbitrary: i)
@@ -809,12 +809,40 @@
     by (auto simp add: length_remove1 dest: length_pos_if_in_set)
 qed
 
-lemma (in linorder) multiset_of_insort [simp]:
-  "multiset_of (insort x xs) = {#x#} + multiset_of xs"
+lemma multiset_of_eq_length_filter:
+  assumes "multiset_of xs = multiset_of ys"
+  shows "length (filter (\<lambda>x. z = x) xs) = length (filter (\<lambda>y. z = y) ys)"
+proof (cases "z \<in># multiset_of xs")
+  case False
+  moreover have "\<not> z \<in># multiset_of ys" using assms False by simp
+  ultimately show ?thesis by (simp add: count_filter)
+next
+  case True
+  moreover have "z \<in># multiset_of ys" using assms True by simp
+  show ?thesis using assms proof (induct xs arbitrary: ys)
+    case Nil then show ?case by simp
+  next
+    case (Cons x xs)
+    from `multiset_of (x # xs) = multiset_of ys` [symmetric]
+      have *: "multiset_of xs = multiset_of (remove1 x ys)"
+      and "x \<in> set ys"
+      by (auto simp add: mem_set_multiset_eq)
+    from * have "length (filter (\<lambda>x. z = x) xs) = length (filter (\<lambda>y. z = y) (remove1 x ys))" by (rule Cons.hyps)
+    moreover from `x \<in> set ys` have "length (filter (\<lambda>y. x = y) ys) > 0" by (simp add: filter_empty_conv)
+    ultimately show ?case using `x \<in> set ys`
+      by (simp add: filter_remove1) (auto simp add: length_remove1)
+  qed
+qed
+
+context linorder
+begin
+
+lemma multiset_of_insort_key [simp]:
+  "multiset_of (insort_key k x xs) = {#x#} + multiset_of xs"
   by (induct xs) (simp_all add: ac_simps)
-
-lemma (in linorder) multiset_of_sort [simp]:
-  "multiset_of (sort xs) = multiset_of xs"
+ 
+lemma multiset_of_sort_key [simp]:
+  "multiset_of (sort_key k xs) = multiset_of xs"
   by (induct xs) (simp_all add: ac_simps)
 
 text {*
@@ -822,18 +850,42 @@
   @{text "f"} with @{text "f xs = ys"} behaves like sort.
 *}
 
-lemma (in linorder) properties_for_sort:
-  "multiset_of ys = multiset_of xs \<Longrightarrow> sorted ys \<Longrightarrow> sort xs = ys"
-proof (induct xs arbitrary: ys)
+lemma properties_for_sort_key:
+  assumes "multiset_of ys = multiset_of xs"
+  and "\<forall>k \<in> f ` set ys. filter (\<lambda>x. k = f x) ys = filter (\<lambda>x. k = f x) xs"
+  and "sorted (map f ys)"
+  shows "sort_key f xs = ys"
+using assms proof (induct xs arbitrary: ys)
   case Nil then show ?case by simp
 next
   case (Cons x xs)
-  then have "x \<in> set ys"
-    by (auto simp add:  mem_set_multiset_eq intro!: ccontr)
-  with Cons.prems Cons.hyps [of "remove1 x ys"] show ?case
-    by (simp add: sorted_remove1 multiset_of_remove1 insort_remove1)
+  from Cons.prems(2) have
+    "\<forall>k \<in> f ` set ys. filter (\<lambda>x. k = f x) (remove1 x ys) = filter (\<lambda>x. k = f x) xs"
+    by (simp add: filter_remove1)
+  with Cons.prems have "sort_key f xs = remove1 x ys"
+    by (auto intro!: Cons.hyps simp add: sorted_map_remove1)
+  moreover from Cons.prems have "x \<in> set ys"
+    by (auto simp add: mem_set_multiset_eq intro!: ccontr)
+  ultimately show ?case using Cons.prems by (simp add: insort_key_remove1)
 qed
 
+lemma properties_for_sort:
+  assumes multiset: "multiset_of ys = multiset_of xs"
+  and "sorted ys"
+  shows "sort xs = ys"
+proof (rule properties_for_sort_key)
+  from multiset show "multiset_of ys = multiset_of xs" .
+  from `sorted ys` show "sorted (map (\<lambda>x. x) ys)" by simp
+  from multiset have "\<And>k. length (filter (\<lambda>y. k = y) ys) = length (filter (\<lambda>x. k = x) xs)"
+    by (rule multiset_of_eq_length_filter)
+  then have "\<And>k. replicate (length (filter (\<lambda>y. k = y) ys)) k = replicate (length (filter (\<lambda>x. k = x) xs)) k"
+    by simp
+  then show "\<forall>k \<in> (\<lambda>x. x) ` set ys. filter (\<lambda>y. k = y) ys = filter (\<lambda>x. k = x) xs"
+    by (simp add: replicate_length_filter)
+qed
+
+end
+
 lemma multiset_of_remdups_le: "multiset_of (remdups xs) \<le> multiset_of xs"
   by (induct xs) (auto intro: order_trans)
 
--- a/src/HOL/List.thy	Sat Sep 18 10:43:52 2010 +0200
+++ b/src/HOL/List.thy	Mon Sep 20 10:29:29 2010 +0200
@@ -3264,6 +3264,10 @@
 apply auto
 done
 
+lemma replicate_length_filter:
+  "replicate (length (filter (\<lambda>y. x = y) xs)) x = filter (\<lambda>y. x = y) xs"
+  by (induct xs) auto
+
 
 subsubsection{*@{text rotate1} and @{text rotate}*}
 
@@ -3738,24 +3742,43 @@
 lemma insort_is_Cons: "\<forall>x\<in>set xs. f a \<le> f x \<Longrightarrow> insort_key f a xs = a # xs"
 by (cases xs) auto
 
+lemma sorted_map_remove1:
+  "sorted (map f xs) \<Longrightarrow> sorted (map f (remove1 x xs))"
+  by (induct xs) (auto simp add: sorted_Cons)
+
 lemma sorted_remove1: "sorted xs \<Longrightarrow> sorted (remove1 a xs)"
-by(induct xs)(auto simp add: sorted_Cons)
-
-lemma insort_key_remove1: "\<lbrakk> a \<in> set xs; sorted (map f xs) ; inj_on f (set xs) \<rbrakk>
-  \<Longrightarrow> insort_key f a (remove1 a xs) = xs"
-proof (induct xs)
+  using sorted_map_remove1 [of "\<lambda>x. x"] by simp
+
+lemma insort_key_remove1:
+  assumes "a \<in> set xs" and "sorted (map f xs)" and "hd (filter (\<lambda>x. f a = f x) xs) = a"
+  shows "insort_key f a (remove1 a xs) = xs"
+using assms proof (induct xs)
   case (Cons x xs)
-  thus ?case
+  then show ?case
   proof (cases "x = a")
     case False
-    hence "f x \<noteq> f a" using Cons.prems by auto
-    hence "f x < f a" using Cons.prems by (auto simp: sorted_Cons)
-    thus ?thesis using Cons by (auto simp: sorted_Cons insort_is_Cons)
+    then have "f x \<noteq> f a" using Cons.prems by auto
+    then have "f x < f a" using Cons.prems by (auto simp: sorted_Cons)
+    with `f x \<noteq> f a` show ?thesis using Cons by (auto simp: sorted_Cons insort_is_Cons)
   qed (auto simp: sorted_Cons insort_is_Cons)
 qed simp
 
-lemma insort_remove1: "\<lbrakk> a \<in> set xs; sorted xs \<rbrakk> \<Longrightarrow> insort a (remove1 a xs) = xs"
-using insort_key_remove1[where f="\<lambda>x. x"] by simp
+lemma insort_remove1:
+  assumes "a \<in> set xs" and "sorted xs"
+  shows "insort a (remove1 a xs) = xs"
+proof (rule insort_key_remove1)
+  from `a \<in> set xs` show "a \<in> set xs" .
+  from `sorted xs` show "sorted (map (\<lambda>x. x) xs)" by simp
+  from `a \<in> set xs` have "a \<in> set (filter (op = a) xs)" by auto
+  then have "set (filter (op = a) xs) \<noteq> {}" by auto
+  then have "filter (op = a) xs \<noteq> []" by (auto simp only: set_empty)
+  then have "length (filter (op = a) xs) > 0" by simp
+  then obtain n where n: "Suc n = length (filter (op = a) xs)"
+    by (cases "length (filter (op = a) xs)") simp_all
+  moreover have "replicate (Suc n) a = a # replicate n a"
+    by simp
+  ultimately show "hd (filter (op = a) xs) = a" by (simp add: replicate_length_filter)
+qed
 
 lemma sorted_remdups[simp]:
   "sorted l \<Longrightarrow> sorted (remdups l)"
--- a/src/HOL/Power.thy	Sat Sep 18 10:43:52 2010 +0200
+++ b/src/HOL/Power.thy	Mon Sep 20 10:29:29 2010 +0200
@@ -29,7 +29,7 @@
 context monoid_mult
 begin
 
-subclass power ..
+subclass power .
 
 lemma power_one [simp]:
   "1 ^ n = 1"
--- a/src/HOL/Predicate_Compile_Examples/Predicate_Compile_Examples.thy	Sat Sep 18 10:43:52 2010 +0200
+++ b/src/HOL/Predicate_Compile_Examples/Predicate_Compile_Examples.thy	Mon Sep 20 10:29:29 2010 +0200
@@ -791,7 +791,7 @@
     "k < l \<Longrightarrow> divmod_rel k l 0 k"
   | "k \<ge> l \<Longrightarrow> divmod_rel (k - l) l q r \<Longrightarrow> divmod_rel k l (Suc q) r"
 
-code_pred divmod_rel ..
+code_pred divmod_rel .
 thm divmod_rel.equation
 value [code] "Predicate.the (divmod_rel_i_i_o_o 1705 42)"
 
--- a/src/HOL/Tools/SMT/smt_translate.ML	Sat Sep 18 10:43:52 2010 +0200
+++ b/src/HOL/Tools/SMT/smt_translate.ML	Mon Sep 20 10:29:29 2010 +0200
@@ -304,18 +304,19 @@
   let val (sels, Us) = split_list (map_index (mk_selector ctxt Ts T n) args)
   in (Const (n, Us ---> T), sels) end
 
-fun lookup_datatype ctxt n Ts = if n = @{type_name bool} then NONE else
-  (case Datatype.get_info (ProofContext.theory_of ctxt) n of
-    NONE => NONE  (* FIXME: also use Record.get_info *)
-  | SOME {descr, ...} =>
-      let
-        val Tds = map (fn (_, (tn, _, _)) => Type (tn, Ts))
-          (sort (int_ord o pairself fst) descr)
-        val Tfs = (case hd descr of (_, (_, tfs, _)) => tfs ~~ Ts)
-      in
-        SOME (descr |> map (fn (i, (_, _, cs)) =>
-          (nth Tds i, map (mk_constructor ctxt (Tds, Tfs) (nth Tds i)) cs)))
-      end)
+fun lookup_datatype ctxt n Ts =
+  if member (op =) [@{type_name bool}, @{type_name nat}] n then NONE
+  else
+    Datatype.get_info (ProofContext.theory_of ctxt) n
+    |> Option.map (fn {descr, ...} =>
+         let
+           val Tds = map (fn (_, (tn, _, _)) => Type (tn, Ts))
+             (sort (int_ord o pairself fst) descr)
+           val Tfs = (case hd descr of (_, (_, tfs, _)) => tfs ~~ Ts)
+         in
+           descr |> map (fn (i, (_, _, cs)) =>
+             (nth Tds i, map (mk_constructor ctxt (Tds, Tfs) (nth Tds i)) cs))
+         end)
 
 fun relaxed thms = (([], thms), map prop_of thms)
 
--- a/src/HOL/Tools/SMT/z3_model.ML	Sat Sep 18 10:43:52 2010 +0200
+++ b/src/HOL/Tools/SMT/z3_model.ML	Mon Sep 20 10:29:29 2010 +0200
@@ -6,7 +6,8 @@
 
 signature Z3_MODEL =
 sig
-  val parse_counterex: SMT_Translate.recon -> string list -> term list
+  val parse_counterex: Proof.context -> SMT_Translate.recon -> string list ->
+    term list
 end
 
 structure Z3_Model: Z3_MODEL =
@@ -15,82 +16,156 @@
 (* counterexample expressions *)
 
 datatype expr = True | False | Number of int * int option | Value of int |
-  Array of array
+  Array of array | App of string * expr list
 and array = Fresh of expr | Store of (array * expr) * expr
 
 
 (* parsing *)
 
 val space = Scan.many Symbol.is_ascii_blank
-fun in_parens p = Scan.$$ "(" |-- p --| Scan.$$ ")"
-fun in_braces p = (space -- Scan.$$ "{") |-- p --| (space -- Scan.$$ "}")
+fun spaced p = p --| space
+fun in_parens p = spaced (Scan.$$ "(") |-- p --| spaced (Scan.$$ ")")
+fun in_braces p = spaced (Scan.$$ "{") |-- p --| spaced (Scan.$$ "}")
 
 val digit = (fn
   "0" => SOME 0 | "1" => SOME 1 | "2" => SOME 2 | "3" => SOME 3 |
   "4" => SOME 4 | "5" => SOME 5 | "6" => SOME 6 | "7" => SOME 7 |
   "8" => SOME 8 | "9" => SOME 9 | _ => NONE)
 
-val nat_num = Scan.repeat1 (Scan.some digit) >>
-  (fn ds => fold (fn d => fn i => i * 10 + d) ds 0)
-val int_num = Scan.optional ($$ "-" >> K (fn i => ~i)) I :|--
-  (fn sign => nat_num >> sign)
+val nat_num = spaced (Scan.repeat1 (Scan.some digit) >>
+  (fn ds => fold (fn d => fn i => i * 10 + d) ds 0))
+val int_num = spaced (Scan.optional ($$ "-" >> K (fn i => ~i)) I :|--
+  (fn sign => nat_num >> sign))
 
 val is_char = Symbol.is_ascii_letter orf Symbol.is_ascii_digit orf
   member (op =) (explode "_+*-/%~=<>$&|?!.@^#")
-val name = Scan.many1 is_char >> implode
+val name = spaced (Scan.many1 is_char >> implode)
+
+fun $$$ s = spaced (Scan.this_string s)
 
-fun array_expr st = st |>
-  in_parens (space |-- (
-  Scan.this_string "const" |-- expr >> Fresh ||
-  Scan.this_string "store" -- space |-- array_expr -- expr -- expr >> Store))
+fun array_expr st = st |> in_parens (
+  $$$ "const" |-- expr >> Fresh ||
+  $$$ "store" |-- array_expr -- expr -- expr >> Store)
 
-and expr st = st |> (space |-- (
-  Scan.this_string "true" >> K True ||
-  Scan.this_string "false" >> K False ||
-  int_num -- Scan.option (Scan.$$ "/" |-- int_num) >> Number ||
-  Scan.this_string "val!" |-- nat_num >> Value ||
-  array_expr >> Array))
+and expr st = st |> (
+  $$$ "true" >> K True ||
+  $$$ "false" >> K False ||
+  int_num -- Scan.option ($$$ "/" |-- int_num) >> Number ||
+  $$$ "val!" |-- nat_num >> Value ||
+  name >> (App o rpair []) ||
+  array_expr >> Array ||
+  in_parens (name -- Scan.repeat1 expr) >> App)
 
-val mapping = space -- Scan.this_string "->"
-val value = mapping |-- expr
-
-val args_case = Scan.repeat expr -- value
-val else_case = space -- Scan.this_string "else" |-- value >>
-  pair ([] : expr list)
+fun args st = ($$$ "->" >> K [] || expr ::: args) st
+val args_case = args -- expr
+val else_case = $$$ "else" -- $$$ "->" |-- expr >> pair ([] : expr list)
 
 val func =
   let fun cases st = (else_case >> single || args_case ::: cases) st
   in in_braces cases end
 
-val cex = space |-- Scan.repeat (space |-- name --| mapping --
-  (func || expr >> (single o pair [])))
+val cex = space |--
+  Scan.repeat (name --| $$$ "->" -- (func || expr >> (single o pair [])))
 
 fun read_cex ls =
-  explode (cat_lines ls)
+  maps (cons "\n" o explode) ls
   |> try (fst o Scan.finite Symbol.stopper cex)
   |> the_default []
 
 
+(* normalization *)
+
+local
+  fun matches terms f n =
+    (case Symtab.lookup terms n of
+      NONE => false
+    | SOME t => f t)
+
+  fun subst f (n, cases) = (n, map (fn (args, v) => (map f args, f v)) cases)
+in
+
+fun reduce_function (n, [c]) = SOME ((n, 0), [c])
+  | reduce_function (n, cases) =
+      let val (patterns, else_case as (_, e)) = split_last cases
+      in
+        (case patterns of
+          [] => NONE
+        | (args, _) :: _ => SOME ((n, length args),
+            filter_out (equal e o snd) patterns @ [else_case]))
+      end
+
+fun drop_skolem_constants terms = filter (Symtab.defined terms o fst o fst)
+
+fun substitute_constants terms =
+  let
+    fun check vs1 [] = rev vs1
+      | check vs1 ((v as ((n, k), [([], Value i)])) :: vs2) =
+          if matches terms (fn Free _ => true | _ => false) n orelse k > 0
+          then check (v :: vs1) vs2
+          else
+            let
+              fun sub (e as Value j) = if i = j then App (n, []) else e
+                | sub e = e
+            in check (map (subst sub) vs1) (map (subst sub) vs2) end
+      | check vs1 (v :: vs2) = check (v :: vs1) vs2
+  in check [] end
+
+fun remove_int_nat_coercions terms vs =
+  let
+    fun match ts ((n, _), _) = matches terms (member (op aconv) ts) n
+
+    val ints =
+      find_first (match [@{term int}]) vs
+      |> Option.map (fn (_, cases) =>
+           let val (cs, (_, e)) = split_last cases
+           in (e, map (apfst hd) cs) end)
+    fun nat_of (v as Value _) = 
+          (case ints of
+            NONE => v
+          | SOME (e, tab) => the_default e (AList.lookup (op =) tab v))
+      | nat_of e = e
+  in
+    map (subst nat_of) vs
+    |> filter_out (match [@{term int}, @{term nat}])
+  end
+
+fun filter_valid_valuations terms = map_filter (fn
+    (_, []) => NONE
+  | ((n, i), cases) =>
+      let
+        fun valid_expr (Array a) = valid_array a
+          | valid_expr (App (n, es)) =
+              Symtab.defined terms n andalso forall valid_expr es
+          | valid_expr _ = true
+        and valid_array (Fresh e) = valid_expr e
+          | valid_array (Store ((a, e1), e2)) =
+              valid_array a andalso valid_expr e1 andalso valid_expr e2
+        fun valid_case (es, e) = forall valid_expr (e :: es)
+      in
+        if not (forall valid_case cases) then NONE
+        else Option.map (rpair cases o rpair i) (Symtab.lookup terms n)
+      end)
+
+end
+
+
 (* translation into terms *)
 
-fun lookup_term tab (name, e) = Option.map (rpair e) (Symtab.lookup tab name)
+fun with_context ctxt terms f vs =
+  fst (fold_map f vs (ctxt, terms, Inttab.empty))
 
-fun with_name_context tab f xs =
-  let
-    val ns = Symtab.fold (Term.add_free_names o snd) tab []
-    val nctxt = Name.make_context ns
-  in fst (fold_map f xs (Inttab.empty, nctxt)) end
+fun fresh_term T (ctxt, terms, values) =
+  let val (n, ctxt') = yield_singleton Variable.variant_fixes "" ctxt
+  in (Free (n, T), (ctxt', terms, values)) end
 
-fun fresh_term T (tab, nctxt) =
-  let val (n, nctxt') = yield_singleton Name.variants "" nctxt
-  in (Free (n, T), (tab, nctxt')) end
-
-fun term_of_value T i (cx as (tab, _)) =
-  (case Inttab.lookup tab i of
+fun term_of_value T i (cx as (_, _, values)) =
+  (case Inttab.lookup values i of
     SOME t => (t, cx)
   | NONE =>
-      let val (t, (tab', nctxt')) = fresh_term T cx
-      in (t, (Inttab.update (i, t) tab', nctxt')) end)
+      let val (t, (ctxt', terms', values')) = fresh_term T cx
+      in (t, (ctxt', terms', Inttab.update (i, t) values')) end)
+
+fun get_term n (cx as (_, terms, _)) = (the (Symtab.lookup terms n), cx)
 
 fun trans_expr _ True = pair @{term True}
   | trans_expr _ False = pair @{term False}
@@ -100,6 +175,13 @@
         HOLogic.mk_number T i $ HOLogic.mk_number T j)
   | trans_expr T (Value i) = term_of_value T i
   | trans_expr T (Array a) = trans_array T a
+  | trans_expr _ (App (n, es)) =
+      let val get_Ts = take (length es) o Term.binder_types o Term.fastype_of
+      in
+        get_term n #-> (fn t =>
+        fold_map (uncurry trans_expr) (get_Ts t ~~ es) #>>
+        Term.list_comb o pair t)
+      end
 
 and trans_array T a =
   let val dT = Term.domain_type T and rT = Term.range_type T
@@ -112,35 +194,60 @@
           Const (@{const_name fun_upd}, [T, dT, rT] ---> T) $ m $ k $ v))
   end
 
-fun trans_pat i T f x =
-  f (Term.domain_type T) ##>> trans (i-1) (Term.range_type T) x #>>
-  (fn (u, (us, t)) => (u :: us, t))
+fun trans_pattern T ([], e) = trans_expr T e #>> pair []
+  | trans_pattern T (arg :: args, e) =
+      trans_expr (Term.domain_type T) arg ##>>
+      trans_pattern (Term.range_type T) (args, e) #>>
+      (fn (arg', (args', e')) => (arg' :: args', e'))
 
-and trans i T ([], v) =
-      if i > 0 then trans_pat i T fresh_term ([], v)
-      else trans_expr T v #>> pair []
-  | trans i T (p :: ps, v) = trans_pat i T (fn U => trans_expr U p) (ps, v)
+fun mk_fun_upd T U = Const (@{const_name fun_upd}, [T --> U, T, U, T] ---> U)
+
+fun split_type T = (Term.domain_type T, Term.range_type T)
 
-fun mk_eq' t us u = HOLogic.mk_eq (Term.list_comb (t, us), u)
-fun mk_eq (Const (@{const_name fun_app}, _)) (u' :: us', u) = mk_eq' u' us' u
-  | mk_eq t (us, u) = mk_eq' t us u
+fun mk_update ([], u) _ = u
+  | mk_update ([t], u) f =
+      uncurry mk_fun_upd (split_type (Term.fastype_of f)) $ f $ t $ u
+  | mk_update (t :: ts, u) f =
+      let
+        val (dT, rT) = split_type (Term.fastype_of f)
+        val (dT', rT') = split_type rT
+      in
+        mk_fun_upd dT rT $ f $ t $
+          mk_update (ts, u) (Term.absdummy (dT', Const ("_", rT')))
+      end
+
+fun mk_lambda Ts (t, pats) =
+  fold_rev (curry Term.absdummy) Ts t |> fold mk_update pats
 
-fun translate (t, cs) =
-  let val T = Term.fastype_of t
-  in
-    (case (can HOLogic.dest_number t, cs) of
-      (true, [c]) => trans 0 T c #>> (fn (_, u) => [mk_eq u ([], t)])
-    | (_, (es, _) :: _) => fold_map (trans (length es) T) cs #>> map (mk_eq t)
-    | _ => raise TERM ("translate: no cases", [t]))
-  end
+fun translate' T i [([], e)] =
+      if i = 0 then trans_expr T e
+      else 
+        let val ((Us1, Us2), U) = Term.strip_type T |>> chop i
+        in trans_expr (Us2 ---> U) e #>> mk_lambda Us1 o rpair [] end
+  | translate' T i cases =
+      let
+        val (pat_cases, def) = split_last cases |> apsnd snd
+        val ((Us1, Us2), U) = Term.strip_type T |>> chop i
+      in
+        trans_expr (Us2 ---> U) def ##>>
+        fold_map (trans_pattern T) pat_cases #>>
+        mk_lambda Us1
+      end
+
+fun translate ((t, i), cases) =
+  translate' (Term.fastype_of t) i cases #>> HOLogic.mk_eq o pair t
 
 
 (* overall procedure *)
 
-fun parse_counterex ({terms, ...} : SMT_Translate.recon) ls =
+fun parse_counterex ctxt ({terms, ...} : SMT_Translate.recon) ls =
   read_cex ls
-  |> map_filter (lookup_term terms)
-  |> with_name_context terms translate
-  |> flat
+  |> map_filter reduce_function
+  |> drop_skolem_constants terms
+  |> substitute_constants terms
+  |> remove_int_nat_coercions terms
+  |> filter_valid_valuations terms
+  |> with_context ctxt terms translate
 
 end
+
--- a/src/HOL/Tools/SMT/z3_solver.ML	Sat Sep 18 10:43:52 2010 +0200
+++ b/src/HOL/Tools/SMT/z3_solver.ML	Mon Sep 20 10:29:29 2010 +0200
@@ -41,11 +41,11 @@
   get_options ctxt
   |> add ["-smt"]
 
-fun raise_cex real recon ls =
-  let val cex = Z3_Model.parse_counterex recon ls
+fun raise_cex ctxt real recon ls =
+  let val cex = Z3_Model.parse_counterex ctxt recon ls
   in raise SMT_Solver.SMT_COUNTEREXAMPLE (real, cex) end
 
-fun if_unsat f (output, recon) =
+fun if_unsat f (output, recon) ctxt =
   let
     fun jnk l =
       String.isPrefix "WARNING" l orelse
@@ -53,13 +53,13 @@
       forall Symbol.is_ascii_blank (Symbol.explode l)
     val (ls, l) = the_default ([], "") (try split_last (filter_out jnk output))
   in
-    if String.isPrefix "unsat" l then f (ls, recon)
-    else if String.isPrefix "sat" l then raise_cex true recon ls
-    else if String.isPrefix "unknown" l then raise_cex false recon ls
+    if String.isPrefix "unsat" l then f (ls, recon) ctxt
+    else if String.isPrefix "sat" l then raise_cex ctxt true recon ls
+    else if String.isPrefix "unknown" l then raise_cex ctxt false recon ls
     else raise SMT_Solver.SMT (solver_name ^ " failed")
   end
 
-val core_oracle = if_unsat (K @{cprop False})
+val core_oracle = uncurry (if_unsat (K (K @{cprop False})))
 
 val prover = if_unsat Z3_Proof_Reconstruction.reconstruct
 
@@ -72,7 +72,7 @@
    {command = {env_var=env_var, remote_name=SOME solver_name},
     arguments = cmdline_options ctxt,
     interface = Z3_Interface.interface with_datatypes,
-    reconstruct = if with_proof then prover else pair o oracle}
+    reconstruct = if with_proof then prover else (fn r => `(oracle o pair r))}
   end
 
 val setup =
--- a/src/Pure/General/binding.ML	Sat Sep 18 10:43:52 2010 +0200
+++ b/src/Pure/General/binding.ML	Mon Sep 20 10:29:29 2010 +0200
@@ -124,10 +124,8 @@
 (* str_of *)
 
 fun str_of binding =
-  let
-    val text = qualified_name_of binding;
-    val props = Position.properties_of (pos_of binding);
-  in Markup.markup (Markup.properties props (Markup.binding (name_of binding))) text end;
+  qualified_name_of binding
+  |> Markup.markup (Position.markup (pos_of binding) (Markup.binding (name_of binding)));
 
 end;
 end;
--- a/src/Pure/General/markup.ML	Sat Sep 18 10:43:52 2010 +0200
+++ b/src/Pure/General/markup.ML	Mon Sep 20 10:29:29 2010 +0200
@@ -30,7 +30,6 @@
   val position_properties': string list
   val position_properties: string list
   val positionN: string val position: T
-  val locationN: string val location: T
   val indentN: string
   val blockN: string val block: int -> T
   val widthN: string
@@ -120,6 +119,7 @@
   val promptN: string val prompt: T
   val readyN: string val ready: T
   val reportN: string val report: T
+  val no_reportN: string val no_report: T
   val badN: string val bad: T
   val no_output: output * output
   val default_output: T -> output * output
@@ -194,7 +194,6 @@
 val position_properties = [lineN, columnN, offsetN] @ position_properties';
 
 val (positionN, position) = markup_elem "position";
-val (locationN, location) = markup_elem "location";
 
 
 (* pretty printing *)
@@ -348,6 +347,7 @@
 val (readyN, ready) = markup_elem "ready";
 
 val (reportN, report) = markup_elem "report";
+val (no_reportN, no_report) = markup_elem "no_report";
 
 val (badN, bad) = markup_elem "bad";
 
--- a/src/Pure/General/markup.scala	Sat Sep 18 10:43:52 2010 +0200
+++ b/src/Pure/General/markup.scala	Mon Sep 20 10:29:29 2010 +0200
@@ -90,7 +90,6 @@
     Set(LINE, COLUMN, OFFSET, END_LINE, END_COLUMN, END_OFFSET, FILE, ID)
 
   val POSITION = "position"
-  val LOCATION = "location"
 
 
   /* pretty printing */
@@ -236,7 +235,6 @@
 
   val INIT = "init"
   val STATUS = "status"
-  val REPORT = "report"
   val WRITELN = "writeln"
   val TRACING = "tracing"
   val WARNING = "warning"
@@ -249,6 +247,9 @@
   val SIGNAL = "signal"
   val EXIT = "exit"
 
+  val REPORT = "report"
+  val NO_REPORT = "no_report"
+
   val BAD = "bad"
 
   val Ready = Markup("ready", Nil)
--- a/src/Pure/General/position.ML	Sat Sep 18 10:43:52 2010 +0200
+++ b/src/Pure/General/position.ML	Mon Sep 20 10:29:29 2010 +0200
@@ -27,7 +27,8 @@
   val of_properties: Properties.T -> T
   val properties_of: T -> Properties.T
   val default_properties: T -> Properties.T -> Properties.T
-  val report_markup: T -> Markup.T
+  val markup: T -> Markup.T -> Markup.T
+  val reported_text: Markup.T -> T -> string -> string
   val report_text: Markup.T -> T -> string -> unit
   val report: Markup.T -> T -> unit
   val str_of: T -> string
@@ -126,12 +127,16 @@
   if exists (member (op =) Markup.position_properties o #1) props then props
   else properties_of default @ props;
 
-fun report_markup pos = Markup.properties (properties_of pos) Markup.report;
+val markup = Markup.properties o properties_of;
+
+
+(* reports *)
 
-fun report_text markup (pos as Pos (count, _)) txt =
-  if invalid_count count then ()
-  else Output.report (Markup.markup (Markup.properties (properties_of pos) markup) txt);
+fun reported_text m (pos as Pos (count, _)) txt =
+  if invalid_count count then ""
+  else Markup.markup (markup pos m) txt;
 
+fun report_text markup pos txt = Output.report (reported_text markup pos txt);
 fun report markup pos = report_text markup pos "";
 
 
--- a/src/Pure/Isar/class.ML	Sat Sep 18 10:43:52 2010 +0200
+++ b/src/Pure/Isar/class.ML	Mon Sep 20 10:29:29 2010 +0200
@@ -630,7 +630,8 @@
   end;
 
 fun default_intro_tac ctxt [] =
-      intro_classes_tac [] ORELSE Locale.intro_locales_tac true ctxt []
+      COND Thm.no_prems no_tac
+        (intro_classes_tac [] ORELSE Locale.intro_locales_tac true ctxt [])
   | default_intro_tac _ _ = no_tac;
 
 fun default_tac rules ctxt facts =
--- a/src/Pure/Isar/proof_context.ML	Sat Sep 18 10:43:52 2010 +0200
+++ b/src/Pure/Isar/proof_context.ML	Mon Sep 20 10:29:29 2010 +0200
@@ -734,8 +734,8 @@
 local
 
 fun parse_failed ctxt pos msg kind =
- (Context_Position.report ctxt Markup.bad pos;
-  cat_error msg ("Failed to parse " ^ kind));
+  cat_error msg ("Failed to parse " ^ kind ^
+    Markup.markup Markup.report (Context_Position.reported_text ctxt Markup.bad pos ""));
 
 fun parse_sort ctxt text =
   let
--- a/src/Pure/Isar/runtime.ML	Sat Sep 18 10:43:52 2010 +0200
+++ b/src/Pure/Isar/runtime.ML	Mon Sep 20 10:29:29 2010 +0200
@@ -61,7 +61,7 @@
           Exn.EXCEPTIONS exns => maps (exn_msgs context) exns
         | CONTEXT (ctxt, exn) => exn_msgs (SOME ctxt) exn
         | EXCURSION_FAIL (exn, loc) =>
-            map (fn msg => msg ^ Markup.markup Markup.location ("\n" ^ loc)) (exn_msgs context exn)
+            map (fn msg => msg ^ Markup.markup Markup.no_report ("\n" ^ loc)) (exn_msgs context exn)
         | TERMINATE => ["Exit"]
         | TimeLimit.TimeOut => ["Timeout"]
         | TOPLEVEL_ERROR => ["Error"]
--- a/src/Pure/ML/ml_compiler_polyml-5.3.ML	Sat Sep 18 10:43:52 2010 +0200
+++ b/src/Pure/ML/ml_compiler_polyml-5.3.ML	Mon Sep 20 10:29:29 2010 +0200
@@ -49,7 +49,7 @@
 
     fun report_decl markup loc decl =
       report_text Markup.ML_ref (offset_position_of loc)
-        (Markup.markup (Markup.properties (Position.properties_of (position_of decl)) markup) "");
+        (Markup.markup (Position.markup (position_of decl) markup) "");
     fun report loc (PolyML.PTtype types) =
           PolyML.NameSpace.displayTypeExpression (types, depth, space)
           |> pretty_ml |> Pretty.from_ML |> Pretty.string_of
@@ -121,10 +121,10 @@
     fun message {message = msg, hard, location = loc, context = _} =
       let
         val txt =
-          Markup.markup Markup.location
+          Markup.markup Markup.no_report
             ((if hard then "Error" else "Warning") ^ Position.str_of (position_of loc) ^ ":\n") ^
           Pretty.string_of (Pretty.from_ML (pretty_ml msg)) ^
-          Markup.markup (Position.report_markup (offset_position_of loc)) "";
+          Position.reported_text Markup.report (offset_position_of loc) "";
       in if hard then err txt else warn txt end;
 
 
--- a/src/Pure/PIDE/command.scala	Sat Sep 18 10:43:52 2010 +0200
+++ b/src/Pure/PIDE/command.scala	Mon Sep 20 10:29:29 2010 +0200
@@ -60,8 +60,10 @@
           atts match {
             case Markup.Serial(i) =>
               val result = XML.Elem(Markup(name, Position.purge(atts)), body)
-              (add_result(i, result) /: Isar_Document.reported_positions(command, message))(
-                (st, range) => st.add_markup(Text.Info(range, result)))
+              val st1 =
+                (add_result(i, result) /: Isar_Document.message_positions(command, message))(
+                  (st, range) => st.add_markup(Text.Info(range, result)))
+              (st1 /: Isar_Document.message_reports(message))(_ accumulate _)
             case _ => System.err.println("Ignored message without serial number: " + message); this
           }
       }
--- a/src/Pure/PIDE/isar_document.scala	Sat Sep 18 10:43:52 2010 +0200
+++ b/src/Pure/PIDE/isar_document.scala	Mon Sep 20 10:29:29 2010 +0200
@@ -56,30 +56,42 @@
   }
 
 
+  /* result messages */
+
+  def clean_message(body: XML.Body): XML.Body =
+    body filter { case XML.Elem(Markup(Markup.NO_REPORT, _), _) => false case _ => true } map
+      { case XML.Elem(markup, ts) => XML.Elem(markup, clean_message(ts)) case t => t }
+
+  def message_reports(msg: XML.Tree): List[XML.Elem] =
+    msg match {
+      case elem @ XML.Elem(Markup(Markup.REPORT, _), _) => List(elem)
+      case XML.Elem(_, body) => body.flatMap(message_reports)
+      case XML.Text(_) => Nil
+    }
+
+
   /* reported positions */
 
-  private val include_pos = Set(Markup.BINDING, Markup.ENTITY, Markup.REPORT, Markup.POSITION)
-  private val exclude_pos = Set(Markup.LOCATION)
-
-  private def is_state(msg: XML.Tree): Boolean =
+  def is_state(msg: XML.Tree): Boolean =
     msg match {
       case XML.Elem(Markup(Markup.WRITELN, _), List(XML.Elem(Markup(Markup.STATE, _), _))) => true
       case _ => false
     }
 
-  def reported_positions(command: Command, message: XML.Elem): Set[Text.Range] =
+  private val include_pos = Set(Markup.BINDING, Markup.ENTITY, Markup.REPORT, Markup.POSITION)
+
+  def message_positions(command: Command, message: XML.Elem): Set[Text.Range] =
   {
-    def reported(set: Set[Text.Range], tree: XML.Tree): Set[Text.Range] =
+    def positions(set: Set[Text.Range], tree: XML.Tree): Set[Text.Range] =
       tree match {
         case XML.Elem(Markup(name, Position.Id_Range(id, raw_range)), body)
         if include_pos(name) && id == command.id =>
           val range = command.decode(raw_range).restrict(command.range)
-          body.foldLeft(if (range.is_singularity) set else set + range)(reported)
-        case XML.Elem(Markup(name, _), body) if !exclude_pos(name) =>
-          body.foldLeft(set)(reported)
+          body.foldLeft(if (range.is_singularity) set else set + range)(positions)
+        case XML.Elem(Markup(name, _), body) => body.foldLeft(set)(positions)
         case _ => set
       }
-    val set = reported(Set.empty, message)
+    val set = positions(Set.empty, message)
     if (set.isEmpty && !is_state(message))
       set ++ Position.Range.unapply(message.markup.properties).map(command.decode(_))
     else set
--- a/src/Pure/System/isabelle_process.scala	Sat Sep 18 10:43:52 2010 +0200
+++ b/src/Pure/System/isabelle_process.scala	Mon Sep 20 10:29:29 2010 +0200
@@ -100,7 +100,8 @@
     if (pid.isEmpty && kind == Markup.INIT)
       pid = props.find(_._1 == Markup.PID).map(_._1)
 
-    xml_cache.cache_tree(XML.Elem(Markup(kind, props), body))((message: XML.Tree) =>
+    val msg = XML.Elem(Markup(kind, props), Isar_Document.clean_message(body))
+    xml_cache.cache_tree(msg)((message: XML.Tree) =>
       receiver ! new Result(message.asInstanceOf[XML.Elem]))
   }
 
--- a/src/Pure/context_position.ML	Sat Sep 18 10:43:52 2010 +0200
+++ b/src/Pure/context_position.ML	Mon Sep 20 10:29:29 2010 +0200
@@ -10,6 +10,7 @@
   val set_visible: bool -> Proof.context -> Proof.context
   val restore_visible: Proof.context -> Proof.context -> Proof.context
   val if_visible: Proof.context -> ('a -> unit) -> 'a -> unit
+  val reported_text: Proof.context -> Markup.T -> Position.T -> string -> string
   val report_text: Proof.context -> Markup.T -> Position.T -> string -> unit
   val report: Proof.context -> Markup.T -> Position.T -> unit
 end;
@@ -29,9 +30,10 @@
 
 fun if_visible ctxt f x = if is_visible ctxt then f x else ();
 
-fun report_text ctxt markup pos txt =
-  if is_visible ctxt then Position.report_text markup pos txt else ();
+fun reported_text ctxt markup pos txt =
+  if is_visible ctxt then Position.reported_text markup pos txt else "";
 
+fun report_text ctxt markup pos txt = Output.report (reported_text ctxt markup pos txt);
 fun report ctxt markup pos = report_text ctxt markup pos "";
 
 end;
--- a/src/Tools/Code/code_printer.ML	Sat Sep 18 10:43:52 2010 +0200
+++ b/src/Tools/Code/code_printer.ML	Mon Sep 20 10:29:29 2010 +0200
@@ -147,13 +147,13 @@
         else s1 ^ s ^ s2
       end;
 
-fun plain_text (XML.Elem (_, xs)) = implode (map plain_text xs)
+fun plain_text (XML.Elem (_, xs)) = maps_string "" plain_text xs
   | plain_text (XML.Text s) = s
 
 fun format presentation_names width =
   Print_Mode.setmp [code_presentationN] (Pretty.string_of_margin width)
   #> YXML.parse_body
-  #> (if null presentation_names then implode o map plain_text
+  #> (if null presentation_names then maps_string "" plain_text
       else maps_string "\n\n" (filter_presentation presentation_names false))
   #> suffix "\n";
 
--- a/src/Tools/Code/code_runtime.ML	Sat Sep 18 10:43:52 2010 +0200
+++ b/src/Tools/Code/code_runtime.ML	Mon Sep 20 10:29:29 2010 +0200
@@ -63,7 +63,7 @@
 fun obtain_serializer thy some_target = Code_Target.produce_code_for thy
   (the_default target some_target) NONE "Code" [];
 
-fun base_evaluator cookie serializer naming thy program ((vs, ty), t) deps args =
+fun base_evaluator cookie serializer (naming : Code_Thingol.naming) thy program ((vs, ty), t) deps args =
   let
     val ctxt = ProofContext.init_global thy;
     val _ = if Code_Thingol.contains_dictvar t then
--- a/src/Tools/jEdit/dist-template/etc/isabelle-jedit.css	Sat Sep 18 10:43:52 2010 +0200
+++ b/src/Tools/jEdit/dist-template/etc/isabelle-jedit.css	Mon Sep 20 10:29:29 2010 +0200
@@ -8,7 +8,7 @@
 .error { background-color: #FFC1C1; }
 .debug { background-color: #FFE4E1; }
 
-.location { display: none; }
+.report { display: none; }
 
 .hilite { background-color: #FFFACD; }