# HG changeset patch
# User huffman
# Date 1257303666 28800
# Node ID c7dfeb7b0b0e9a9d081db5a15ab795bacfed9fdf
# Parent  42d7b6b4992ba291f10a3ccf41621e74171feee1
better error handling for fixrec_simp

diff -r 42d7b6b4992b -r c7dfeb7b0b0e src/HOLCF/Tools/fixrec.ML
--- a/src/HOLCF/Tools/fixrec.ML	Tue Nov 03 18:33:16 2009 -0800
+++ b/src/HOLCF/Tools/fixrec.ML	Tue Nov 03 19:01:06 2009 -0800
@@ -379,21 +379,19 @@
   let
     val tab = FixrecUnfoldData.get (Context.Proof ctxt);
     val ss = FixrecSimpData.get (Context.Proof ctxt);
-    (* TODO: fail gracefully if t has the wrong form *)
     fun concl t =
       if Logic.is_all t then concl (snd (Logic.dest_all t))
       else HOLogic.dest_Trueprop (Logic.strip_imp_concl t);
-    fun unfold_thm t =
-      case chead_of (fst (HOLogic.dest_eq (concl t))) of
-        Const (c, T) => Symtab.lookup tab c
-      | t => NONE;
     fun tac (t, i) =
-      case unfold_thm t of
-        SOME thm => rtac (thm RS @{thm ssubst_lhs}) i THEN
-                         asm_simp_tac ss i
-      | NONE => asm_simp_tac ss i;
+      let
+        val Const (c, T) = chead_of (fst (HOLogic.dest_eq (concl t)));
+        val unfold_thm = the (Symtab.lookup tab c);
+        val rule = unfold_thm RS @{thm ssubst_lhs};
+      in
+        CHANGED (rtac rule i THEN asm_simp_tac ss i)
+      end
   in
-    SUBGOAL tac
+    SUBGOAL (fn ti => tac ti handle _ => no_tac)
   end;
 
 val fixrec_simp_add : Thm.attribute =