tuned
authortraytel
Mon, 26 Aug 2013 14:14:33 +0200
changeset 53204 cf40231bc305
parent 53203 222ea6acbdd6
child 53209 1d248d75620e
tuned
src/HOL/BNF/Tools/bnf_fp_util.ML
--- a/src/HOL/BNF/Tools/bnf_fp_util.ML	Mon Aug 26 13:44:46 2013 +0200
+++ b/src/HOL/BNF/Tools/bnf_fp_util.ML	Mon Aug 26 14:14:33 2013 +0200
@@ -48,8 +48,6 @@
   val corecN: string
   val ctorN: string
   val ctor_dtorN: string
-  val ctor_dtor_corecN: string
-  val ctor_dtor_unfoldN: string
   val ctor_exhaustN: string
   val ctor_induct2N: string
   val ctor_inductN: string
@@ -272,7 +270,6 @@
 val dtor_unfold_o_mapN = dtor_unfoldN ^ "_o_" ^ mapN
 val ctor_fold_transferN = ctor_foldN ^ transferN
 val dtor_unfold_transferN = dtor_unfoldN ^ transferN
-val ctor_dtor_unfoldN = ctorN ^ "_" ^ dtor_unfoldN
 val ctor_mapN = ctorN ^ "_" ^ mapN
 val dtor_mapN = dtorN ^ "_" ^ mapN
 val map_uniqueN = mapN ^ uniqueN
@@ -305,7 +302,6 @@
 val dtor_corecN = dtorN ^ "_" ^ corecN
 val dtor_corec_o_mapN = dtor_corecN ^ "_o_" ^ mapN
 val dtor_corec_uniqueN = dtor_corecN ^ uniqueN
-val ctor_dtor_corecN = ctorN ^ "_" ^ dtor_corecN
 
 val ctor_dtorN = ctorN ^ "_" ^ dtorN
 val dtor_ctorN = dtorN ^ "_" ^ ctorN