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/BNF/bnf_lfp_rec_sugar.ML
changeset 58388 4d408eb71301
parent 58387 bc35a30cf0f2
child 58389 ee1f45ca0d73 
--- a/src/HOL/Tools/BNF/bnf_lfp_rec_sugar.ML	Fri Sep 19 13:27:04 2014 +0200
+++ b/src/HOL/Tools/BNF/bnf_lfp_rec_sugar.ML	Fri Sep 19 13:27:04 2014 +0200
@@ -32,7 +32,6 @@
      fp_res_index: int,
      C: typ,
      fun_arg_Tsss : typ list list list,
-     ctr_defs: thm list,
      ctr_sugar: Ctr_Sugar.ctr_sugar,
      recx: term,
      rec_thms: thm list};
@@ -109,7 +108,6 @@
    fp_res_index: int,
    C: typ,
    fun_arg_Tsss : typ list list list,
-   ctr_defs: thm list,
    ctr_sugar: ctr_sugar,
    recx: term,
    rec_thms: thm list};
isabelle