--- a/src/HOL/BNF/Tools/bnf_fp_def_sugar.ML Fri Aug 16 15:35:47 2013 +0200
+++ b/src/HOL/BNF/Tools/bnf_fp_def_sugar.ML Fri Aug 16 15:49:16 2013 +0200
@@ -272,7 +272,7 @@
let
fun build (TU as (T, U)) =
if T = U then
- id_const T
+ HOLogic.id_const T
else
(case TU of
(Type (s, Ts), Type (s', Us)) =>
--- a/src/HOL/BNF/Tools/bnf_fp_util.ML Fri Aug 16 15:35:47 2013 +0200
+++ b/src/HOL/BNF/Tools/bnf_fp_util.ML Fri Aug 16 15:49:16 2013 +0200
@@ -140,7 +140,7 @@
val mk_sumTN: typ list -> typ
val mk_sumTN_balanced: typ list -> typ
- val id_const: typ -> term
+ val mk_convol: term * term -> term
val Inl_const: typ -> typ -> term
val Inr_const: typ -> typ -> term
@@ -372,7 +372,12 @@
val mk_sumTN = Library.foldr1 mk_sumT;
val mk_sumTN_balanced = Balanced_Tree.make mk_sumT;
-fun id_const T = Const (@{const_name id}, T --> T);
+fun mk_convol (f, g) =
+ let
+ val (fU, fTU) = `range_type (fastype_of f);
+ val ((gT, gU), gTU) = `dest_funT (fastype_of g);
+ val convolT = fTU --> gTU --> gT --> HOLogic.mk_prodT (fU, gU);
+ in Const (@{const_name convol}, convolT) $ f $ g end;
fun Inl_const LT RT = Const (@{const_name Inl}, LT --> mk_sumT (LT, RT));
fun mk_Inl RT t = Inl_const (fastype_of t) RT $ t;
--- a/src/HOL/BNF/Tools/bnf_lfp_util.ML Fri Aug 16 15:35:47 2013 +0200
+++ b/src/HOL/BNF/Tools/bnf_lfp_util.ML Fri Aug 16 15:49:16 2013 +0200
@@ -12,7 +12,6 @@
val mk_bij_betw: term -> term -> term -> term
val mk_cardSuc: term -> term
- val mk_convol: term * term -> term
val mk_cpow: term -> term
val mk_inver: term -> term -> term -> term
val mk_not_empty: term -> term
@@ -66,11 +65,4 @@
fun mk_not_empty B = mk_not_eq B (HOLogic.mk_set (HOLogic.dest_setT (fastype_of B)) []);
-fun mk_convol (f, g) =
- let
- val (fU, fTU) = `range_type (fastype_of f);
- val ((gT, gU), gTU) = `dest_funT (fastype_of g);
- val convolT = fTU --> gTU --> gT --> HOLogic.mk_prodT (fU, gU);
- in Const (@{const_name convol}, convolT) $ f $ g end;
-
end;