src/HOLCF/Tools/fixrec_package.ML
changeset 31174 f1f1e9b53c81
parent 31095 b79d140f6d0b
child 31177 c39994cb152a
     1.1 --- a/src/HOLCF/Tools/fixrec_package.ML	Sat May 16 15:24:35 2009 +0200
     1.2 +++ b/src/HOLCF/Tools/fixrec_package.ML	Sat May 16 20:17:59 2009 +0200
     1.3 @@ -195,7 +195,7 @@
     1.4      val unfold_thms = unfolds names tuple_unfold_thm;
     1.5      fun mk_note (n, thm) = ((Binding.name n, []), [thm]);
     1.6      val (thmss, lthy'') = lthy'
     1.7 -      |> fold_map (LocalTheory.note Thm.theoremK o mk_note)
     1.8 +      |> fold_map (LocalTheory.note Thm.generated_theoremK o mk_note)
     1.9          ((all_names ^ "_induct", tuple_induct_thm) :: unfold_thms);
    1.10    in
    1.11      (lthy'', names, fixdef_thms, map snd unfold_thms)
    1.12 @@ -373,7 +373,7 @@
    1.13        val simps2 : (Attrib.binding * thm list) list =
    1.14          map (apsnd (fn thm => [thm])) (List.concat simps);
    1.15        val (_, lthy'') = lthy'
    1.16 -        |> fold_map (LocalTheory.note Thm.theoremK) (simps1 @ simps2);
    1.17 +        |> fold_map (LocalTheory.note Thm.generated_theoremK) (simps1 @ simps2);
    1.18      in
    1.19        lthy''
    1.20      end