src/HOL/Tools/primrec_package.ML
changeset 31174 f1f1e9b53c81
parent 31172 74d72ba262fb
child 31177 c39994cb152a
     1.1 --- a/src/HOL/Tools/primrec_package.ML	Sat May 16 15:24:35 2009 +0200
     1.2 +++ b/src/HOL/Tools/primrec_package.ML	Sat May 16 20:17:59 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.theoremK) simps)
     1.8 -    |-> (fn simps' => LocalTheory.note Thm.theoremK
     1.9 +    |-> (fn simps => fold_map (LocalTheory.note Thm.generated_theoremK) simps)
    1.10 +    |-> (fn simps' => LocalTheory.note Thm.generated_theoremK
    1.11            ((qualify (Binding.qualified_name "simps"), simp_atts), maps snd simps'))
    1.12      |>> snd
    1.13    end handle PrimrecError (msg, some_eqn) =>