defer evaluation of Scan.message, for improved performance in the frequent situation where failure is handled later (e.g. via ||);

--- a/src/HOL/Boogie/Tools/boogie_loader.ML	Sat Jul 23 16:12:12 2011 +0200
+++ b/src/HOL/Boogie/Tools/boogie_loader.ML	Sat Jul 23 16:37:17 2011 +0200
@@ -331,18 +331,19 @@
 
 fun stopper i = Scan.stopper (K (i, EOF)) (fn (_, EOF) => true | _ => false)
 
-fun scan_err msg [] = "Boogie (at end of input): " ^ msg
-  | scan_err msg ((i, _) :: _) = "Boogie (at line " ^ string_of_int i ^ "): " ^
-      msg
+fun scan_err msg [] = (fn () => "Boogie (at end of input): " ^ msg ())
+  | scan_err msg ((i, _) :: _) =
+      (fn () => "Boogie (at line " ^ string_of_int i ^ "): " ^ msg ())
 
-fun scan_fail msg = Scan.fail_with (scan_err msg)
+fun scan_fail' msg = Scan.fail_with (scan_err msg)
+fun scan_fail s = scan_fail' (fn () => s)
 
 fun finite scan fold_lines input =
   let val (i, ts) = tokenize fold_lines input
   in
     (case Scan.error (Scan.finite (stopper i) scan) ts of
       (x, []) => x
-    | (_, ts') => error (scan_err "unparsed input" ts'))
+    | (_, ts') => error ((scan_err (fn () => "unparsed input") ts') ()))
   end
 
 fun read_int' s = (case read_int (raw_explode s) of (i, []) => SOME i | _ => NONE)
@@ -361,7 +362,7 @@
 fun scan_lookup kind tab key =
   (case Symtab.lookup tab key of
     SOME value => Scan.succeed value
-  | NONE => scan_fail ("undefined " ^ kind ^ ": " ^ quote key))
+  | NONE => scan_fail' (fn () => "undefined " ^ kind ^ ": " ^ quote key))
 
 fun typ tds =
   let

--- a/src/HOL/SPARK/Tools/fdl_lexer.ML	Sat Jul 23 16:12:12 2011 +0200
+++ b/src/HOL/SPARK/Tools/fdl_lexer.ML	Sat Jul 23 16:37:17 2011 +0200
@@ -194,9 +194,9 @@
     fun get_pos [] = " (past end-of-text!)"
       | get_pos ((_, pos) :: _) = Position.str_of pos;
 
-    fun err (syms, msg) =
+    fun err (syms, msg) = fn () =>
       text ^ get_pos syms ^ " at " ^ beginning 10 (map symbol syms) ^
-      (case msg of NONE => "" | SOME s => "\n" ^ s);
+        (case msg of NONE => "" | SOME m => "\n" ^ m ());
   in Scan.!! err scan end;
 
 val any_line' =

--- a/src/HOL/SPARK/Tools/fdl_parser.ML	Sat Jul 23 16:12:12 2011 +0200
+++ b/src/HOL/SPARK/Tools/fdl_parser.ML	Sat Jul 23 16:37:17 2011 +0200
@@ -72,10 +72,10 @@
     fun get_pos [] = " (past end-of-file!)"
       | get_pos (tok :: _) = Fdl_Lexer.pos_of tok;
 
-    fun err (syms, msg) =
+    fun err (syms, msg) = fn () =>
       "Syntax error" ^ get_pos syms ^ " at " ^
-      beginning 10 (map Fdl_Lexer.unparse syms) ^
-      (case msg of NONE => "" | SOME s => "\n" ^ s ^ " expected");
+        beginning 10 (map Fdl_Lexer.unparse syms) ^
+        (case msg of NONE => "" | SOME m => "\n" ^ m () ^ " expected");
   in Scan.!! err scan end;
 
 fun parse_all p =
@@ -84,7 +84,7 @@
 
 (** parsers **)
 
-fun group s p = p || Scan.fail_with (K s);
+fun group s p = p || Scan.fail_with (K (fn () => s));
 
 fun $$$ s = group s
   (Scan.one (fn t => Fdl_Lexer.kind_of t = Fdl_Lexer.Keyword andalso

--- a/src/Pure/General/antiquote.ML	Sat Jul 23 16:12:12 2011 +0200
+++ b/src/Pure/General/antiquote.ML	Sat Jul 23 16:37:17 2011 +0200
@@ -83,7 +83,7 @@
 
 val scan_antiq =
   Symbol_Pos.scan_pos -- ($$$ "@" |-- $$$ "{" |--
-    Symbol_Pos.!!! "missing closing brace of antiquotation"
+    Symbol_Pos.!!! (fn () => "missing closing brace of antiquotation")
       (Scan.repeat scan_ant -- ($$$ "}" |-- Symbol_Pos.scan_pos)))
   >> (fn (pos1, (body, pos2)) => (flat body, Position.range pos1 pos2));
 

--- a/src/Pure/General/scan.ML	Sat Jul 23 16:12:12 2011 +0200
+++ b/src/Pure/General/scan.ML	Sat Jul 23 16:37:17 2011 +0200
@@ -11,8 +11,9 @@
 
 signature BASIC_SCAN =
 sig
+  type message = unit -> string
   (*error msg handler*)
-  val !! : ('a * string option -> string) -> ('a -> 'b) -> 'a -> 'b
+  val !! : ('a * message option -> message) -> ('a -> 'b) -> 'a -> 'b
   (*apply function*)
   val >> : ('a -> 'b * 'c) * ('b -> 'd) -> 'a -> 'd * 'c
   (*alternative*)
@@ -41,7 +42,7 @@
   val error: ('a -> 'b) -> 'a -> 'b
   val catch: ('a -> 'b) -> 'a -> 'b    (*exception Fail*)
   val fail: 'a -> 'b
-  val fail_with: ('a -> string) -> 'a -> 'b
+  val fail_with: ('a -> message) -> 'a -> 'b
   val succeed: 'a -> 'b -> 'a * 'b
   val some: ('a -> 'b option) -> 'a list -> 'b * 'a list
   val one: ('a -> bool) -> 'a list -> 'a * 'a list
@@ -93,19 +94,21 @@
 
 (* exceptions *)
 
+type message = unit -> string;
+
 exception MORE of string option;        (*need more input (prompt)*)
-exception FAIL of string option;        (*try alternatives (reason of failure)*)
-exception ABORT of string;              (*dead end*)
+exception FAIL of message option;       (*try alternatives (reason of failure)*)
+exception ABORT of message;             (*dead end*)
 
 fun !! err scan xs = scan xs handle FAIL msg => raise ABORT (err (xs, msg));
 fun permissive scan xs = scan xs handle MORE _ => raise FAIL NONE | ABORT _ => raise FAIL NONE;
 fun strict scan xs = scan xs handle MORE _ => raise FAIL NONE;
 fun prompt str scan xs = scan xs handle MORE NONE => raise MORE (SOME str);
-fun error scan xs = scan xs handle ABORT msg => Library.error msg;
+fun error scan xs = scan xs handle ABORT msg => Library.error (msg ());
 
 fun catch scan xs = scan xs
-  handle ABORT msg => raise Fail msg
-    | FAIL msg => raise Fail (the_default "Syntax error" msg);
+  handle ABORT msg => raise Fail (msg ())
+    | FAIL msg => raise Fail (case msg of NONE => "Syntax error" | SOME m => m ());
 
 
 (* scanner combinators *)
@@ -236,7 +239,7 @@
 
 fun finite' (Stopper (mk_stopper, is_stopper)) scan (state, input) =
   let
-    fun lost () = raise ABORT "Bad scanner: lost stopper of finite scan!";
+    fun lost () = raise ABORT (fn () => "Bad scanner: lost stopper of finite scan!");
 
     fun stop [] = lost ()
       | stop lst =
@@ -244,7 +247,7 @@
           in if is_stopper x then ((), xs) else lost () end;
   in
     if exists is_stopper input then
-      raise ABORT "Stopper may not occur in input of finite scan!"
+      raise ABORT (fn () => "Stopper may not occur in input of finite scan!")
     else (strict scan --| lift stop) (state, input @ [mk_stopper input])
   end;
 

--- a/src/Pure/General/symbol.ML	Sat Jul 23 16:12:12 2011 +0200
+++ b/src/Pure/General/symbol.ML	Sat Jul 23 16:37:17 2011 +0200
@@ -404,13 +404,13 @@
 
 fun scanner msg scan chs =
   let
-    fun message (cs, NONE) = msg ^ ": " ^ quote (beginning 10 cs)
-      | message (cs, SOME msg') = msg ^ ", " ^ msg' ^ ": " ^ quote (beginning 10 cs);
+    fun message (cs, NONE) = (fn () => msg ^ ": " ^ quote (beginning 10 cs))
+      | message (cs, SOME msg') = (fn () => msg ^ ", " ^ msg' () ^ ": " ^ quote (beginning 10 cs));
     val fin_scan = Scan.error (Scan.finite stopper (!! message scan));
   in
     (case fin_scan chs of
       (result, []) => result
-    | (_, rest) => error (message (rest, NONE)))
+    | (_, rest) => error (message (rest, NONE) ()))
   end;
 
 val scan_id = Scan.one is_letter ^^ (Scan.many is_letdig >> implode);

--- a/src/Pure/General/symbol_pos.ML	Sat Jul 23 16:12:12 2011 +0200
+++ b/src/Pure/General/symbol_pos.ML	Sat Jul 23 16:37:17 2011 +0200
@@ -13,7 +13,7 @@
   val content: T list -> string
   val is_eof: T -> bool
   val stopper: T Scan.stopper
-  val !!! : string -> (T list -> 'a) -> T list -> 'a
+  val !!! : Scan.message -> (T list -> 'a) -> T list -> 'a
   val change_prompt: ('a -> 'b) -> 'a -> 'b
   val scan_pos: T list -> Position.T * T list
   val scan_string_q: T list -> (Position.T * (T list * Position.T)) * T list
@@ -65,9 +65,9 @@
     fun get_pos [] = " (past end-of-text!)"
       | get_pos ((_, pos) :: _) = Position.str_of pos;
 
-    fun err (syms, msg) =
-      text ^ get_pos syms ^ " at " ^ Symbol.beginning 10 (map symbol syms) ^
-      (case msg of NONE => "" | SOME s => "\n" ^ s);
+    fun err (syms, msg) = fn () =>
+      text () ^ get_pos syms ^ " at " ^ Symbol.beginning 10 (map symbol syms) ^
+      (case msg of NONE => "" | SOME m => "\n" ^ m ());
   in Scan.!! err scan end;
 
 fun change_prompt scan = Scan.prompt "# " scan;
@@ -91,11 +91,11 @@
     in if n <= 255 then Scan.succeed [(chr n, pos)] else Scan.fail end);
 
 fun scan_str q =
-  $$$ "\\" |-- !!! "bad escape character in string" ($$$ q || $$$ "\\" || char_code) ||
+  $$$ "\\" |-- !!! (fn () => "bad escape character in string") ($$$ q || $$$ "\\" || char_code) ||
   Scan.one (fn (s, _) => s <> q andalso s <> "\\" andalso Symbol.is_regular s) >> single;
 
 fun scan_strs q =
-  (scan_pos --| $$$ q) -- !!! "missing quote at end of string"
+  (scan_pos --| $$$ q) -- !!! (fn () => "missing quote at end of string")
     (change_prompt ((Scan.repeat (scan_str q) >> flat) -- ($$$ q |-- scan_pos)));
 
 in

--- a/src/Pure/General/xml.ML	Sat Jul 23 16:12:12 2011 +0200
+++ b/src/Pure/General/xml.ML	Sat Jul 23 16:37:17 2011 +0200
@@ -138,8 +138,8 @@
 
 local
 
-fun err s (xs, _) =
-  "XML parsing error: " ^ s ^ "\nfound: " ^ quote (Symbol.beginning 100 xs);
+fun err msg (xs, _) =
+  fn () => "XML parsing error: " ^ msg () ^ "\nfound: " ^ quote (Symbol.beginning 100 xs);
 
 fun ignored _ = [];
 
@@ -202,10 +202,10 @@
 and parse_element xs =
   ($$ "<" |-- Symbol.scan_id --
     Scan.repeat (blanks |-- parse_att) --| blanks :-- (fn (s, _) =>
-      !! (err "Expected > or />")
+      !! (err (fn () => "Expected > or />"))
         (Scan.this_string "/>" >> ignored
          || $$ ">" |-- parse_content --|
-            !! (err ("Expected </" ^ s ^ ">"))
+            !! (err (fn () => "Expected </" ^ s ^ ">"))
               (Scan.this_string ("</" ^ s) --| blanks --| $$ ">"))) >> Elem) xs;
 
 val parse_document =
@@ -213,7 +213,7 @@
   |-- parse_element;
 
 fun parse s =
-  (case Scan.finite Symbol.stopper (Scan.error (!! (err "Malformed element")
+  (case Scan.finite Symbol.stopper (Scan.error (!! (err (fn () => "Malformed element"))
       (blanks |-- parse_document --| blanks))) (raw_explode s) of
     (x, []) => x
   | (_, ys) => error ("XML parsing error: Unprocessed input\n" ^ Symbol.beginning 100 ys));

--- a/src/Pure/Isar/isar_syn.ML	Sat Jul 23 16:12:12 2011 +0200
+++ b/src/Pure/Isar/isar_syn.ML	Sat Jul 23 16:37:17 2011 +0200
@@ -775,8 +775,8 @@
     (props_text :|-- (fn (pos, str) =>
       (case Outer_Syntax.parse pos str of
         [tr] => Scan.succeed (K tr)
-      | _ => Scan.fail_with (K "exactly one command expected"))
-      handle ERROR msg => Scan.fail_with (K msg)));
+      | _ => Scan.fail_with (K (fn () => "exactly one command expected")))
+      handle ERROR msg => Scan.fail_with (K (fn () => msg))));
 
 
 

--- a/src/Pure/Isar/parse.ML	Sat Jul 23 16:12:12 2011 +0200
+++ b/src/Pure/Isar/parse.ML	Sat Jul 23 16:37:17 2011 +0200
@@ -115,13 +115,14 @@
 (* group atomic parsers (no cuts!) *)
 
 fun fail_with s = Scan.fail_with
-  (fn [] => s ^ " expected (past end-of-file!)"
+  (fn [] => (fn () => s ^ " expected (past end-of-file!)")
     | tok :: _ =>
-        (case Token.text_of tok of
-          (txt, "") =>
-            s ^ " expected,\nbut " ^ txt ^ Token.pos_of tok ^ " was found"
-        | (txt1, txt2) =>
-            s ^ " expected,\nbut " ^ txt1 ^ Token.pos_of tok ^ " was found:\n" ^ txt2));
+        (fn () =>
+          (case Token.text_of tok of
+            (txt, "") =>
+              s ^ " expected,\nbut " ^ txt ^ Token.pos_of tok ^ " was found"
+          | (txt1, txt2) =>
+              s ^ " expected,\nbut " ^ txt1 ^ Token.pos_of tok ^ " was found:\n" ^ txt2)));
 
 fun group s scan = scan || fail_with s;
 
@@ -133,10 +134,13 @@
     fun get_pos [] = " (past end-of-file!)"
       | get_pos (tok :: _) = Token.pos_of tok;
 
-    fun err (toks, NONE) = kind ^ get_pos toks
+    fun err (toks, NONE) = (fn () => kind ^ get_pos toks)
       | err (toks, SOME msg) =
-          if String.isPrefix kind msg then msg
-          else kind ^ get_pos toks ^ ": " ^ msg;
+          (fn () =>
+            let val s = msg () in
+              if String.isPrefix kind s then s
+              else kind ^ get_pos toks ^ ": " ^ s
+            end);
   in Scan.!! err scan end;
 
 fun !!! scan = cut "Outer syntax error" scan;

--- a/src/Pure/Isar/token.ML	Sat Jul 23 16:12:12 2011 +0200
+++ b/src/Pure/Isar/token.ML	Sat Jul 23 16:37:17 2011 +0200
@@ -50,7 +50,6 @@
   val assign: value option -> T -> unit
   val closure: T -> T
   val ident_or_symbolic: string -> bool
-  val !!! : string -> (Symbol_Pos.T list -> 'a) -> Symbol_Pos.T list -> 'a
   val source_proper: (T, 'a) Source.source -> (T, (T, 'a) Source.source) Source.source
   val source': {do_recover: bool Option.option} -> (unit -> Scan.lexicon * Scan.lexicon) ->
     (Symbol_Pos.T, 'a) Source.source -> (T, (Symbol_Pos.T, 'a) Source.source) Source.source
@@ -257,7 +256,7 @@
 
 open Basic_Symbol_Pos;
 
-fun !!! msg = Symbol_Pos.!!! ("Outer lexical error: " ^ msg);
+fun !!! msg = Symbol_Pos.!!! (fn () => "Outer lexical error: " ^ msg);
 
 
 (* scan symbolic idents *)

--- a/src/Pure/ML/ml_lex.ML	Sat Jul 23 16:12:12 2011 +0200
+++ b/src/Pure/ML/ml_lex.ML	Sat Jul 23 16:37:17 2011 +0200
@@ -136,7 +136,7 @@
 
 open Basic_Symbol_Pos;
 
-fun !!! msg = Symbol_Pos.!!! ("SML lexical error: " ^ msg);
+fun !!! msg = Symbol_Pos.!!! (fn () => "SML lexical error: " ^ msg);
 
 
 (* blanks *)

--- a/src/Pure/ML/ml_parse.ML	Sat Jul 23 16:12:12 2011 +0200
+++ b/src/Pure/ML/ml_parse.ML	Sat Jul 23 16:37:17 2011 +0200
@@ -20,13 +20,13 @@
     fun get_pos [] = " (past end-of-file!)"
       | get_pos (tok :: _) = Position.str_of (ML_Lex.pos_of tok);
 
-    fun err (toks, NONE) = "SML syntax error" ^ get_pos toks
-      | err (toks, SOME msg) = "SML syntax error" ^ get_pos toks ^ ": " ^ msg;
+    fun err (toks, NONE) = (fn () => "SML syntax error" ^ get_pos toks)
+      | err (toks, SOME msg) = (fn () => "SML syntax error" ^ get_pos toks ^ ": " ^ msg ());
   in Scan.!! err scan end;
 
 fun bad_input x =
   (Scan.some (fn tok => (case ML_Lex.kind_of tok of ML_Lex.Error msg => SOME msg | _ => NONE)) :|--
-    (fn msg => Scan.fail_with (K msg))) x;
+    (fn msg => Scan.fail_with (K (fn () => msg)))) x;
 
 
 (** basic parsers **)

--- a/src/Pure/Syntax/lexicon.ML	Sat Jul 23 16:12:12 2011 +0200
+++ b/src/Pure/Syntax/lexicon.ML	Sat Jul 23 16:37:17 2011 +0200
@@ -114,7 +114,7 @@
 
 open Basic_Symbol_Pos;
 
-fun !!! msg = Symbol_Pos.!!! ("Inner lexical error: " ^ msg);
+fun !!! msg = Symbol_Pos.!!! (fn () => "Inner lexical error: " ^ msg);
 
 val scan_id =
   Scan.one (Symbol.is_letter o Symbol_Pos.symbol) :::

--- a/src/Pure/Thy/rail.ML	Sat Jul 23 16:12:12 2011 +0200
+++ b/src/Pure/Thy/rail.ML	Sat Jul 23 16:37:17 2011 +0200
@@ -72,7 +72,7 @@
 
 val scan =
   (Scan.repeat scan_token >> flat) --|
-    Symbol_Pos.!!! "Rail lexical error: bad input"
+    Symbol_Pos.!!! (fn () => "Rail lexical error: bad input")
       (Scan.ahead (Scan.one Symbol_Pos.is_eof));
 
 in
@@ -92,17 +92,20 @@
     fun get_pos [] = " (past end-of-file!)"
       | get_pos (tok :: _) = Position.str_of (pos_of tok);
 
-    fun err (toks, NONE) = prefix ^ get_pos toks
+    fun err (toks, NONE) = (fn () => prefix ^ get_pos toks)
       | err (toks, SOME msg) =
-          if String.isPrefix prefix msg then msg
-          else prefix ^ get_pos toks ^ ": " ^ msg;
+          (fn () =>
+            let val s = msg () in
+              if String.isPrefix prefix s then s
+              else prefix ^ get_pos toks ^ ": " ^ s
+            end);
   in Scan.!! err scan end;
 
 fun $$$ x =
   Scan.one (fn tok => kind_of tok = Keyword andalso content_of tok = x) ||
   Scan.fail_with
-    (fn [] => print_keyword x ^ " expected (past end-of-file!)"
-      | tok :: _ => print_keyword x ^ " expected,\nbut " ^ print tok ^ " was found");
+    (fn [] => (fn () => print_keyword x ^ " expected (past end-of-file!)")
+      | tok :: _ => (fn () => print_keyword x ^ " expected,\nbut " ^ print tok ^ " was found"));
 
 fun enum1 sep scan = scan ::: Scan.repeat ($$$ sep |-- !!! scan);
 fun enum sep scan = enum1 sep scan || Scan.succeed [];

--- a/src/Pure/Thy/thy_output.ML	Sat Jul 23 16:12:12 2011 +0200
+++ b/src/Pure/Thy/thy_output.ML	Sat Jul 23 16:37:17 2011 +0200
@@ -355,7 +355,7 @@
   Scan.depend (fn d => opt_newline |-- Scan.one Token.is_begin_ignore
     >> pair (d + 1)) ||
   Scan.depend (fn d => Scan.one Token.is_end_ignore --|
-    (if d = 0 then Scan.fail_with (K "Bad nesting of meta-comments") else opt_newline)
+    (if d = 0 then Scan.fail_with (K (fn () => "Bad nesting of meta-comments")) else opt_newline)
     >> pair (d - 1));
 
 val tag = (improper -- Parse.$$$ "%" -- improper) |-- Parse.!!! (Parse.tag_name --| blank_end);

--- a/src/Tools/Code/code_printer.ML	Sat Jul 23 16:12:12 2011 +0200
+++ b/src/Tools/Code/code_printer.ML	Sat Jul 23 16:37:17 2011 +0200
@@ -101,7 +101,8 @@
 
 (** generic nonsense *)
 
-fun eqn_error (SOME thm) s = error (s ^ ",\nin equation " ^ Display.string_of_thm_without_context thm)
+fun eqn_error (SOME thm) s =
+      error (s ^ ",\nin equation " ^ Display.string_of_thm_without_context thm)
   | eqn_error NONE s = error s;
 
 val code_presentationN = "code_presentation";
@@ -132,10 +133,10 @@
 
 fun filter_presentation [] tree =
       Buffer.empty
-      |> fold XML.add_content tree 
+      |> fold XML.add_content tree
   | filter_presentation presentation_names tree =
       let
-        fun is_selected (name, attrs) = 
+        fun is_selected (name, attrs) =
           name = code_presentationN
           andalso member (op =) presentation_names (the (Properties.get attrs stmt_nameN));
         fun add_content_with_space tree (is_first, buf) =
@@ -169,8 +170,9 @@
     val namemap' = fold2 (curry Symtab.update) names names' namemap;
   in (namemap', namectxt') end;
 
-fun lookup_var (namemap, _) name = case Symtab.lookup namemap name
- of SOME name' => name'
+fun lookup_var (namemap, _) name =
+  case Symtab.lookup namemap name of
+    SOME name' => name'
   | NONE => error ("Invalid name in context: " ^ quote name);
 
 val first_upper = implode o nth_map 0 Symbol.to_ascii_upper o raw_explode;
@@ -190,7 +192,7 @@
     val vars' = intro_vars fished3 vars;
   in map (lookup_var vars') fished3 end;
 
-fun intro_base_names no_syntax deresolve names = names 
+fun intro_base_names no_syntax deresolve names = names
   |> map_filter (fn name => if no_syntax name then
       let val name' = deresolve name in
         if Long_Name.is_qualified name' then NONE else SOME name'
@@ -297,7 +299,8 @@
   | requires_args (complex_const_syntax (k, _)) = k;
 
 fun simple_const_syntax syn =
-  complex_const_syntax (apsnd (fn f => ([], (fn _ => fn _ => fn print => fn _ => fn vars => f (print vars)))) syn);
+  complex_const_syntax
+    (apsnd (fn f => ([], (fn _ => fn _ => fn print => fn _ => fn vars => f (print vars)))) syn);
 
 type activated_complex_const_syntax = int * ((var_ctxt -> fixity -> iterm -> Pretty.T)
   -> thm option -> var_ctxt -> fixity -> (iterm * itype) list -> Pretty.T)
@@ -311,20 +314,24 @@
       fold_map (Code_Thingol.ensure_declared_const thy) cs naming
       |-> (fn cs' => pair (Complex_const_syntax (n, f literals cs')));
 
-fun gen_print_app print_app_expr print_term const_syntax some_thm vars fxy (app as ((c, (_, function_typs)), ts)) =
-  case const_syntax c
-   of NONE => brackify fxy (print_app_expr some_thm vars app)
-    | SOME (Plain_const_syntax (_, s)) => brackify fxy (str s :: map (print_term some_thm vars BR) ts)
-    | SOME (Complex_const_syntax (k, print)) =>
-        let
-          fun print' fxy ts = print (print_term some_thm) some_thm vars fxy (ts ~~ take k function_typs);
-        in if k = length ts
-          then print' fxy ts
+fun gen_print_app print_app_expr print_term const_syntax some_thm vars fxy
+    (app as ((c, (_, function_typs)), ts)) =
+  case const_syntax c of
+    NONE => brackify fxy (print_app_expr some_thm vars app)
+  | SOME (Plain_const_syntax (_, s)) =>
+      brackify fxy (str s :: map (print_term some_thm vars BR) ts)
+  | SOME (Complex_const_syntax (k, print)) =>
+      let
+        fun print' fxy ts =
+          print (print_term some_thm) some_thm vars fxy (ts ~~ take k function_typs);
+      in
+        if k = length ts
+        then print' fxy ts
         else if k < length ts
-          then case chop k ts of (ts1, ts2) =>
-            brackify fxy (print' APP ts1 :: map (print_term some_thm vars BR) ts2)
-          else print_term some_thm vars fxy (Code_Thingol.eta_expand k app)
-        end;
+        then case chop k ts of (ts1, ts2) =>
+          brackify fxy (print' APP ts1 :: map (print_term some_thm vars BR) ts2)
+        else print_term some_thm vars fxy (Code_Thingol.eta_expand k app)
+      end;
 
 fun gen_print_bind print_term thm (fxy : fixity) pat vars =
   let
@@ -377,12 +384,14 @@
            (   $$ "'" |-- sym_any
             || Scan.unless ($$ "_" || $$ "/" || $$ "(" |-- $$ "_" |-- $$ ")")
                  sym_any) >> (String o implode)));
-  in case Scan.finite Symbol.stopper parse (Symbol.explode s)
-   of ((false, [String s]), []) => mk_plain s
+    fun err s (_, NONE) = (fn () => "malformed mixfix annotation: " ^ quote s)
+      | err _ (_, SOME msg) = msg;
+  in
+    case Scan.finite Symbol.stopper parse (Symbol.explode s) of
+      ((false, [String s]), []) => mk_plain s
     | ((_, p as [_]), []) => mk_complex (mk_mixfix prep_arg (NOBR, p))
     | ((b, p as _ :: _ :: _), []) => mk_complex (mk_mixfix prep_arg (if b then NOBR else BR, p))
-    | _ => Scan.!!
-        (the_default ("malformed mixfix annotation: " ^ quote s) o snd) Scan.fail ()
+    | _ => Scan.!! (err s) Scan.fail ()
   end;
 
 val (infixK, infixlK, infixrK) = ("infix", "infixl", "infixr");

--- a/src/Tools/WWW_Find/unicode_symbols.ML	Sat Jul 23 16:12:12 2011 +0200
+++ b/src/Tools/WWW_Find/unicode_symbols.ML	Sat Jul 23 16:37:17 2011 +0200
@@ -103,12 +103,13 @@
       Scan.literal keywords >> token Keyword ||
       scan_ascii_symbol ||
       Lexicon.scan_id >> token Name;
-    val scan_token = Symbol_Pos.!!! "Lexical error" (Scan.bulk scanner);
+    val scan_token = Symbol_Pos.!!! (fn () => "Lexical error") (Scan.bulk scanner);
   in
     (case Scan.error (Scan.finite Symbol_Pos.stopper scan_token) syms of
       (toks, []) => toks
-    | (_, ss) => error ("Lexical error at: " ^ Symbol_Pos.content ss
-                        ^ Position.str_of (#1 (Symbol_Pos.range ss))))
+    | (_, ss) =>
+        error ("Lexical error at: " ^ Symbol_Pos.content ss ^
+          Position.str_of (#1 (Symbol_Pos.range ss))))
   end;
 
 val stopper =