--- a/src/HOLCF/Tools/fixrec_package.ML Wed Mar 19 18:15:25 2008 +0100
+++ b/src/HOLCF/Tools/fixrec_package.ML Wed Mar 19 22:27:57 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 (Name (cname^"_unfold"));
+ val unfold_thm = PureThy.get_thm thy (Facts.Named (cname^"_unfold", NONE));
val simp = Goal.prove_global thy [] [] eq
(fn _ => EVERY [stac unfold_thm 1, simp_tac (simpset_of thy) 1]);
in simp end;