bstring -> binding

--- a/src/HOL/Tools/function_package/fundef_common.ML	Mon Mar 30 16:37:23 2009 +0200
+++ b/src/HOL/Tools/function_package/fundef_common.ML	Mon Mar 30 16:37:23 2009 +0200
@@ -65,7 +65,7 @@
       defname : string,
 
       (* contains no logical entities: invariant under morphisms *)
-      add_simps : (string -> string) -> string -> Attrib.src list -> thm list 
+      add_simps : (binding -> binding) -> string -> Attrib.src list -> thm list 
                   -> local_theory -> thm list * local_theory,
       case_names : string list,
 
@@ -289,7 +289,7 @@
 (* Preprocessors *)
 
 type fixes = ((string * typ) * mixfix) list
-type 'a spec = ((bstring * Attrib.src list) * 'a list) list
+type 'a spec = (Attrib.binding * 'a list) list
 type preproc = fundef_config -> Proof.context -> fixes -> term spec 
                -> (term list * (thm list -> thm spec) * (thm list -> thm list list) * string list)
 
@@ -303,7 +303,7 @@
 
 fun empty_preproc check _ ctxt fixes spec =
     let 
-      val (nas,tss) = split_list spec
+      val (bnds, tss) = split_list spec
       val ts = flat tss
       val _ = check ctxt fixes ts
       val fnames = map (fst o fst) fixes
@@ -314,9 +314,9 @@
                         |> map (map snd)
 
       (* using theorem names for case name currently disabled *)
-      val cnames = map_index (fn (i, (n,_)) => mk_case_names i "" 1) nas |> flat
+      val cnames = map_index (fn (i, _) => mk_case_names i "" 1) bnds |> flat
     in
-      (ts, curry op ~~ nas o Library.unflat tss, sort, cnames)
+      (ts, curry op ~~ bnds o Library.unflat tss, sort, cnames)
     end
 
 structure Preprocessor = GenericDataFun

--- a/src/HOL/Tools/function_package/fundef_datatype.ML	Mon Mar 30 16:37:23 2009 +0200
+++ b/src/HOL/Tools/function_package/fundef_datatype.ML	Mon Mar 30 16:37:23 2009 +0200
@@ -252,7 +252,7 @@
 fun sequential_preproc (config as FundefConfig {sequential, ...}) ctxt fixes spec =
       if sequential then
         let
-          val (nas, eqss) = split_list spec
+          val (bnds, eqss) = split_list spec
                             
           val eqs = map the_single eqss
                     
@@ -266,9 +266,9 @@
                            (FundefSplit.split_all_equations ctxt compleqs)
 
           fun restore_spec thms =
-              nas ~~ Library.take (length nas, Library.unflat spliteqs thms)
+              bnds ~~ Library.take (length bnds, Library.unflat spliteqs thms)
               
-          val spliteqs' = flat (Library.take (length nas, spliteqs))
+          val spliteqs' = flat (Library.take (length bnds, spliteqs))
           val fnames = map (fst o fst) fixes
           val indices = map (fn eq => find_index (curry op = (fname_of eq)) fnames) spliteqs'
 
@@ -276,11 +276,11 @@
                                        |> map (map snd)
 
 
-          val nas' = nas @ replicate (length spliteqs - length nas) ("",[])
+          val bnds' = bnds @ replicate (length spliteqs - length bnds) Attrib.empty_binding
 
           (* using theorem names for case name currently disabled *)
-          val case_names = map_index (fn (i, ((n, _), es)) => mk_case_names i "" (length es)) 
-                                     (nas' ~~ spliteqs)
+          val case_names = map_index (fn (i, (_, es)) => mk_case_names i "" (length es)) 
+                                     (bnds' ~~ spliteqs)
                            |> flat
         in
           (flat spliteqs, restore_spec, sort, case_names)

--- 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