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/BNF/Tools/bnf_fp.ML
changeset 51839 5c552de1d8d1
parent 51837 087498724486 
--- a/src/HOL/BNF/Tools/bnf_fp.ML	Tue Apr 30 13:45:43 2013 +0200
+++ b/src/HOL/BNF/Tools/bnf_fp.ML	Tue Apr 30 15:58:32 2013 +0200
@@ -10,8 +10,8 @@
 sig
   type fp_result =
     {bnfs: BNF_Def.bnf list,
+     ctors: term list,
      dtors: term list,
-     ctors: term list,
      folds: term list,
      recs: term list,
      induct: thm,
@@ -25,6 +25,7 @@
      fold_thms: thm list,
      rec_thms: thm list}
 
+  val fp_name_of_ctor: term -> string
   val morph_fp_result: morphism -> fp_result -> fp_result
   val eq_fp_result: fp_result * fp_result -> bool
 
@@ -173,8 +174,8 @@
 
 type fp_result =
   {bnfs: BNF_Def.bnf list,
+   ctors: term list,
    dtors: term list,
-   ctors: term list,
    folds: term list,
    recs: term list,
    induct: thm,
@@ -188,11 +189,13 @@
    fold_thms: thm list,
    rec_thms: thm list};
 
-fun morph_fp_result phi {bnfs, dtors, ctors, folds, recs, induct, strong_induct, dtor_ctors,
+val fp_name_of_ctor = fst o dest_Type o range_type o fastype_of;
+
+fun morph_fp_result phi {bnfs, ctors, dtors, folds, recs, induct, strong_induct, dtor_ctors,
     ctor_dtors, ctor_injects, map_thms, set_thmss, rel_thms, fold_thms, rec_thms} =
   {bnfs = map (morph_bnf phi) bnfs,
+   ctors = map (Morphism.term phi) ctors,
    dtors = map (Morphism.term phi) dtors,
-   ctors = map (Morphism.term phi) ctors,
    folds = map (Morphism.term phi) folds,
    recs = map (Morphism.term phi) recs,
    induct = Morphism.thm phi induct,
isabelle