--- a/src/HOL/Tools/primrec_package.ML Wed Mar 11 15:38:25 2009 +0100
+++ b/src/HOL/Tools/primrec_package.ML Wed Mar 11 15:42:19 2009 +0100
@@ -260,7 +260,7 @@
|-> (fn defs => `(fn ctxt => prove_spec ctxt names1 rec_rewrites defs spec'))
|-> (fn simps => fold_map (LocalTheory.note Thm.theoremK) simps)
|-> (fn simps' => LocalTheory.note Thm.theoremK
- ((qualify (Binding.name "simps"), simp_atts), maps snd simps'))
+ ((qualify (Binding.qualified_name "simps"), simp_atts), maps snd simps'))
|>> snd
end handle PrimrecError (msg, some_eqn) =>
error ("Primrec definition error:\n" ^ msg ^ (case some_eqn