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/Nominal/nominal_primrec.ML
changeset 29006 abe0f11cfa4e
parent 28965 1de908189869
child 29097 68245155eb58 
--- a/src/HOL/Nominal/nominal_primrec.ML	Fri Dec 05 18:42:39 2008 +0100
+++ b/src/HOL/Nominal/nominal_primrec.ML	Fri Dec 05 18:43:42 2008 +0100
@@ -230,7 +230,7 @@
 fun gen_primrec_i note def alt_name invs fctxt eqns_atts thy =
   let
     val (raw_eqns, atts) = split_list eqns_atts;
-    val eqns = map (apfst Name.name_of) raw_eqns;
+    val eqns = map (apfst Binding.base_name) raw_eqns;
     val dt_info = NominalPackage.get_nominal_datatypes thy;
     val rec_eqns = fold_rev (process_eqn thy o snd) eqns [];
     val lsrs :: lsrss = maps (fn (_, (_, _, eqns)) =>
isabelle