--- a/Quot/Examples/Larry.thy	Fri Dec 11 06:58:31 2009 +0100
+++ b/Quot/Examples/Larry.thy	Fri Dec 11 08:28:41 2009 +0100
@@ -354,7 +354,7 @@
       and C: "\<And>K X. P X \<Longrightarrow> P (Crypt K X)"
       and D: "\<And>K X. P X \<Longrightarrow> P (Decrypt K X)"
   shows "P msg"
-using N M C D by (blast intro:  msg_induct_aux)
+using N M C D by (rule msg_induct_aux)
 
 subsection{*The Abstract Discriminator*}
 

--- a/Quot/QuotMain.thy	Fri Dec 11 06:58:31 2009 +0100
+++ b/Quot/QuotMain.thy	Fri Dec 11 08:28:41 2009 +0100
@@ -5,7 +5,6 @@
      ("quotient_def.ML")
 begin
 
-
 locale QUOT_TYPE =
   fixes R :: "'a \<Rightarrow> 'a \<Rightarrow> bool"
   and   Abs :: "('a \<Rightarrow> bool) \<Rightarrow> 'b"
@@ -1021,10 +1020,10 @@
 let
   val rtrm_str = Syntax.string_of_term ctxt rtrm
   val qtrm_str = Syntax.string_of_term ctxt qtrm
-  val msg = [enclose "[" "]" fun_str, "The quotient theorem\n", qtrm_str, 
-             "and the lifted theorem\n", rtrm_str, "do not match"]
+  val msg = cat_lines [enclose "[" "]" fun_str, "The quotient theorem", qtrm_str, 
+             "", "does not match with original theorem", rtrm_str]
 in
-  error (space_implode " " msg)
+  error msg
 end
 *}