# HG changeset patch
# User traytel
# Date 1376660956 -7200
# Node ID 953534445ab6067e3999cb32b3704d916b2d83f2
# Parent  83cbe188855acfe8b1928de78709c05d29ab87c0
tuned

diff -r 83cbe188855a -r 953534445ab6 src/HOL/BNF/Tools/bnf_fp_def_sugar.ML
--- 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)) =>
diff -r 83cbe188855a -r 953534445ab6 src/HOL/BNF/Tools/bnf_fp_util.ML
--- 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;
diff -r 83cbe188855a -r 953534445ab6 src/HOL/BNF/Tools/bnf_lfp_util.ML
--- 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;