src/HOLCF/Tools/fixrec_package.ML
changeset 26343 0dd2eab7b296
parent 26336 a0e2b706ce73
child 26939 1035c89b4c02
     1.1 --- a/src/HOLCF/Tools/fixrec_package.ML	Wed Mar 19 22:50:42 2008 +0100
     1.2 +++ b/src/HOLCF/Tools/fixrec_package.ML	Thu Mar 20 00:20:44 2008 +0100
     1.3 @@ -267,7 +267,7 @@
     1.4      val eq = mk_trp (HOLogic.eq_const T $ t $ Var (("x",0),T));
     1.5      val cname = case chead_of t of Const(c,_) => c | _ =>
     1.6                fixrec_err "function is not declared as constant in theory";
     1.7 -    val unfold_thm = PureThy.get_thm thy (Facts.Named (cname^"_unfold", NONE));
     1.8 +    val unfold_thm = PureThy.get_thm thy (cname^"_unfold");
     1.9      val simp = Goal.prove_global thy [] [] eq
    1.10            (fn _ => EVERY [stac unfold_thm 1, simp_tac (simpset_of thy) 1]);
    1.11    in simp end;