src/HOL/Tools/primrec_package.ML
changeset 31177 c39994cb152a
parent 31174 f1f1e9b53c81
child 31262 580510315dda
     1.1 --- a/src/HOL/Tools/primrec_package.ML	Sun May 17 07:17:39 2009 +0200
     1.2 +++ b/src/HOL/Tools/primrec_package.ML	Mon May 18 09:48:06 2009 +0200
     1.3 @@ -253,8 +253,8 @@
     1.4      |> set_group ? LocalTheory.set_group (serial_string ())
     1.5      |> fold_map (LocalTheory.define Thm.definitionK o make_def lthy fixes fs) defs
     1.6      |-> (fn defs => `(fn ctxt => prove_spec ctxt names1 rec_rewrites defs spec'))
     1.7 -    |-> (fn simps => fold_map (LocalTheory.note Thm.generated_theoremK) simps)
     1.8 -    |-> (fn simps' => LocalTheory.note Thm.generated_theoremK
     1.9 +    |-> (fn simps => fold_map (LocalTheory.note Thm.generatedK) simps)
    1.10 +    |-> (fn simps' => LocalTheory.note Thm.generatedK
    1.11            ((qualify (Binding.qualified_name "simps"), simp_atts), maps snd simps'))
    1.12      |>> snd
    1.13    end handle PrimrecError (msg, some_eqn) =>