--- a/src/HOLCF/Tools/fixrec_package.ML Wed Mar 19 22:50:42 2008 +0100
+++ b/src/HOLCF/Tools/fixrec_package.ML Thu Mar 20 00:20:44 2008 +0100
@@ -267,7 +267,7 @@
val eq = mk_trp (HOLogic.eq_const T $ t $ Var (("x",0),T));
val cname = case chead_of t of Const(c,_) => c | _ =>
fixrec_err "function is not declared as constant in theory";
- val unfold_thm = PureThy.get_thm thy (Facts.Named (cname^"_unfold", NONE));
+ val unfold_thm = PureThy.get_thm thy (cname^"_unfold");
val simp = Goal.prove_global thy [] [] eq
(fn _ => EVERY [stac unfold_thm 1, simp_tac (simpset_of thy) 1]);
in simp end;