diff -r 216a839841bc -r 0f1e85fcf5f4 src/HOL/Matrix/ComputeHOL.thy
--- a/src/HOL/Matrix/ComputeHOL.thy	Sat Mar 17 11:57:03 2012 +0100
+++ b/src/HOL/Matrix/ComputeHOL.thy	Sat Mar 17 11:59:59 2012 +0100
@@ -150,7 +150,7 @@
 local
 fun lhs_of eq = fst (Thm.dest_equals (cprop_of eq));
 in
-fun rewrite_conv [] ct = raise CTERM ("rewrite_conv", [])
+fun rewrite_conv [] ct = raise CTERM ("rewrite_conv", [ct])
   | rewrite_conv (eq :: eqs) ct =
       Thm.instantiate (Thm.match (lhs_of eq, ct)) eq
       handle Pattern.MATCH => rewrite_conv eqs ct;