src/HOL/Nominal/nominal_primrec.ML
changeset 31177 c39994cb152a
parent 31174 f1f1e9b53c81
child 31723 f5cafe803b55
     1.1 --- a/src/HOL/Nominal/nominal_primrec.ML	Sun May 17 07:17:39 2009 +0200
     1.2 +++ b/src/HOL/Nominal/nominal_primrec.ML	Mon May 18 09:48:06 2009 +0200
     1.3 @@ -367,11 +367,11 @@
     1.4        (fn thss => fn goal_ctxt =>
     1.5           let
     1.6             val simps = ProofContext.export goal_ctxt lthy' (flat thss);
     1.7 -           val (simps', lthy'') = fold_map (LocalTheory.note Thm.generated_theoremK)
     1.8 +           val (simps', lthy'') = fold_map (LocalTheory.note Thm.generatedK)
     1.9               (names_atts' ~~ map single simps) lthy'
    1.10           in
    1.11             lthy''
    1.12 -           |> LocalTheory.note Thm.generated_theoremK ((qualify (Binding.name "simps"),
    1.13 +           |> LocalTheory.note Thm.generatedK ((qualify (Binding.name "simps"),
    1.14                  map (Attrib.internal o K)
    1.15                      [Simplifier.simp_add, Nitpick_Const_Simp_Thms.add]),
    1.16                  maps snd simps')