diff -r bdcabcffaaf6 -r e49bfeb0d822 src/HOLCF/Tools/fixrec.ML --- a/src/HOLCF/Tools/fixrec.ML Fri Nov 13 15:48:52 2009 +0100 +++ b/src/HOLCF/Tools/fixrec.ML Fri Nov 13 17:25:09 2009 +0100 @@ -242,8 +242,7 @@ ((thm_name, [src]), [thm]) end; val (thmss, lthy'') = lthy' - |> fold_map (LocalTheory.note Thm.generatedK) - (induct_note :: map unfold_note unfold_thms); + |> fold_map (LocalTheory.note "") (induct_note :: map unfold_note unfold_thms); in (lthy'', names, fixdef_thms, map snd unfold_thms) end; @@ -465,7 +464,7 @@ val simps2 : (Attrib.binding * thm list) list = map (apsnd (fn thm => [thm])) (flat simps); val (_, lthy'') = lthy' - |> fold_map (LocalTheory.note Thm.generatedK) (simps1 @ simps2); + |> fold_map (LocalTheory.note "") (simps1 @ simps2); in lthy'' end