Mercurial Mercurial > repos > isabelle / diff
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/HOL/Tools/function_package/fundef_package.ML
changeset 29006 abe0f11cfa4e
parent 28965 1de908189869
child 29051 b9c5726e79ab 
--- a/src/HOL/Tools/function_package/fundef_package.ML	Fri Dec 05 18:42:39 2008 +0100
+++ b/src/HOL/Tools/function_package/fundef_package.ML	Fri Dec 05 18:43:42 2008 +0100
@@ -96,8 +96,8 @@
 fun gen_add_fundef is_external prep fixspec eqnss config flags lthy =
     let
       val ((fixes0, spec0), ctxt') = prep fixspec (map (fn (n_a, eq) => [(n_a, [eq])]) eqnss) lthy
-      val fixes = map (apfst (apfst Name.name_of)) fixes0;
-      val spec = map (apfst (apfst Name.name_of)) spec0;
+      val fixes = map (apfst (apfst Binding.base_name)) fixes0;
+      val spec = map (apfst (apfst Binding.base_name)) spec0;
       val (eqs, post, sort_cont, cnames) = FundefCommon.get_preproc lthy config flags ctxt' fixes spec
 
       val defname = mk_defname fixes
isabelle