diff -r b6f6948bdcf1 -r 350bb108406d src/HOL/Tools/function_package/fundef_package.ML
--- a/src/HOL/Tools/function_package/fundef_package.ML	Mon Mar 30 16:37:23 2009 +0200
+++ b/src/HOL/Tools/function_package/fundef_package.ML	Mon Mar 30 16:37:23 2009 +0200
@@ -55,7 +55,7 @@
                    |> map (apfst (apfst extra_qualify))
 
       val (saved_spec_simps, lthy) =
-        fold_map note_theorem spec lthy
+        fold_map (LocalTheory.note Thm.theoremK) spec lthy
 
       val saved_simps = flat (map snd saved_spec_simps)
       val simps_by_f = sort saved_simps
@@ -78,7 +78,7 @@
 
       val (((psimps', pinducts'), (_, [termination'])), lthy) =
           lthy
-            |> addsmps (Long_Name.qualify "partial") "psimps"
+            |> addsmps (Binding.qualify false "partial") "psimps"
                  psimp_attribs psimps
             ||> fold_option (snd oo addsmps I "simps" simp_attribs) trsimps
             ||>> note_theorem ((qualify "pinduct",
@@ -106,7 +106,7 @@
       val constrn_fxs = map (fn (b, T, mx) => (b, SOME (the_default default_constraint T), mx))
       val ((fixes0, spec0), ctxt') = prep (constrn_fxs fixspec) eqns lthy
       val fixes = map (apfst (apfst Binding.name_of)) fixes0;
-      val spec = map (fn ((b, atts), prop) => ((Binding.name_of b, atts), [prop])) spec0;
+      val spec = map (fn (bnd, prop) => (bnd, [prop])) spec0;
       val (eqs, post, sort_cont, cnames) = FundefCommon.get_preproc lthy config ctxt' fixes spec
 
       val defname = mk_defname fixes