src/HOLCF/Tools/fixrec.ML
changeset 33666 e49bfeb0d822
parent 33522 737589bb9bb8
child 33670 02b7738aef6a
--- 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