--- a/src/HOLCF/Tools/fixrec_package.ML Sat May 16 15:24:35 2009 +0200
+++ b/src/HOLCF/Tools/fixrec_package.ML Sat May 16 20:17:59 2009 +0200
@@ -195,7 +195,7 @@
val unfold_thms = unfolds names tuple_unfold_thm;
fun mk_note (n, thm) = ((Binding.name n, []), [thm]);
val (thmss, lthy'') = lthy'
- |> fold_map (LocalTheory.note Thm.theoremK o mk_note)
+ |> fold_map (LocalTheory.note Thm.generated_theoremK o mk_note)
((all_names ^ "_induct", tuple_induct_thm) :: unfold_thms);
in
(lthy'', names, fixdef_thms, map snd unfold_thms)
@@ -373,7 +373,7 @@
val simps2 : (Attrib.binding * thm list) list =
map (apsnd (fn thm => [thm])) (List.concat simps);
val (_, lthy'') = lthy'
- |> fold_map (LocalTheory.note Thm.theoremK) (simps1 @ simps2);
+ |> fold_map (LocalTheory.note Thm.generated_theoremK) (simps1 @ simps2);
in
lthy''
end