1.1 --- a/src/HOL/Matrix/ComputeHOL.thy	Sat Mar 17 11:57:03 2012 +0100
     1.2 +++ b/src/HOL/Matrix/ComputeHOL.thy	Sat Mar 17 11:59:59 2012 +0100
     1.3 @@ -150,7 +150,7 @@
     1.4  local
     1.5  fun lhs_of eq = fst (Thm.dest_equals (cprop_of eq));
     1.6  in
     1.7 -fun rewrite_conv [] ct = raise CTERM ("rewrite_conv", [])
     1.8 +fun rewrite_conv [] ct = raise CTERM ("rewrite_conv", [ct])
     1.9    | rewrite_conv (eq :: eqs) ct =
    1.10        Thm.instantiate (Thm.match (lhs_of eq, ct)) eq
    1.11        handle Pattern.MATCH => rewrite_conv eqs ct;