fixrec shows unsolved subgoals when proofs of rewrites fail

--- a/src/HOLCF/Fixrec.thy	Sat Jun 18 00:33:27 2005 +0200
+++ b/src/HOLCF/Fixrec.thy	Sat Jun 18 00:38:18 2005 +0200
@@ -179,10 +179,16 @@
 lemma cpair_eqD2: "<x,y> = <x',y'> \<Longrightarrow> y = y'"
 by simp
 
+text {* lemma for proving rewrite rules *}
+
+lemma ssubst_lhs: "\<lbrakk>t = s; P s = Q\<rbrakk> \<Longrightarrow> P t = Q"
+by simp
+
 ML {*
 val cpair_equalI = thm "cpair_equalI";
 val cpair_eqD1 = thm "cpair_eqD1";
 val cpair_eqD2 = thm "cpair_eqD2";
+val ssubst_lhs = thm "ssubst_lhs";
 *}
 
 subsection {* Intitializing the fixrec package *}

--- a/src/HOLCF/fixrec_package.ML	Sat Jun 18 00:33:27 2005 +0200
+++ b/src/HOLCF/fixrec_package.ML	Sat Jun 18 00:38:18 2005 +0200
@@ -210,8 +210,7 @@
     val ss = simpset_of thy;
     val ct = cterm_of thy t;
     val thm = prove_goalw_cterm [] ct
-      (fn _ => [SOLVE(stac unfold_thm 1 THEN simp_tac ss 1)])
-        handle _ => sys_error (string_of_cterm ct^" :: proof failed on this equation.");
+      (fn _ => [rtac (unfold_thm RS ssubst_lhs) 1, simp_tac ss 1]);
   in thm end;
 
 (* this proves that each equation is a theorem *)