src/ZF/Tools/primrec_package.ML

 Package for defining functions on datatypes by primitive recursion
 *)
 
 signature PRIMREC_PACKAGE =
 sig
-  val add_primrec: ((bstring * string) * Attrib.src list) list -> theory -> theory * thm list
-  val add_primrec_i: ((bstring * term) * attribute list) list -> theory -> theory * thm list
+  val add_primrec: ((Name.binding * string) * Attrib.src list) list -> theory -> theory * thm list
+  val add_primrec_i: ((Name.binding * term) * attribute list) list -> theory -> theory * thm list
 end;
 
 structure PrimrecPackage : PRIMREC_PACKAGE =
 struct
 

         Goal.prove_global thy1 [] [] (Ind_Syntax.traceIt "next primrec equation = " thy1 t)
           (fn _ => EVERY [rewrite_goals_tac rewrites, rtac refl 1]));
 
     val (eqn_thms', thy2) =
       thy1
-      |> PureThy.add_thms ((eqn_names ~~ eqn_thms) ~~ eqn_atts);
+      |> PureThy.add_thms ((map Name.name_of eqn_names ~~ eqn_thms) ~~ eqn_atts);
     val (_, thy3) =
       thy2
       |> PureThy.add_thmss [(("simps", eqn_thms'), [Simplifier.simp_add])]
       ||> Sign.parent_path;
   in (thy3, eqn_thms') end;