# HG changeset patch
# User krauss
# Date 1258985159 -3600
# Node ID cd8acf137c9c9a54d746ede368a015fd977cc4f8
# Parent  26a4cb3a7eaed52684f24a3e4421814013749b7a
eliminated dead code and some unused bindings, reported by polyml

diff -r 26a4cb3a7eae -r cd8acf137c9c src/HOL/Tools/Function/decompose.ML
--- a/src/HOL/Tools/Function/decompose.ML	Mon Nov 23 13:45:16 2009 +0100
+++ b/src/HOL/Tools/Function/decompose.ML	Mon Nov 23 15:05:59 2009 +0100
@@ -74,7 +74,7 @@
      | _ => no_tac)
   | _ => no_tac)
 
-fun decompose_tac' ctxt cont err_cont D = Termination.CALLS (fn (cs, i) =>
+fun decompose_tac' cont err_cont D = Termination.CALLS (fn (cs, i) =>
     let
       val G = mk_dgraph D cs
       val sccs = TermGraph.strong_conn G
@@ -94,12 +94,7 @@
 
 fun decompose_tac ctxt chain_tac cont err_cont =
     derive_chains ctxt chain_tac
-    (decompose_tac' ctxt cont err_cont)
-
-fun auto_decompose_tac ctxt =
-    Termination.TERMINATION ctxt
-      (decompose_tac ctxt (auto_tac (clasimpset_of ctxt))
-                     (K (K all_tac)) (K (K no_tac)))
+    (decompose_tac' cont err_cont)
 
 
 end
diff -r 26a4cb3a7eae -r cd8acf137c9c src/HOL/Tools/Function/fun.ML
--- a/src/HOL/Tools/Function/fun.ML	Mon Nov 23 13:45:16 2009 +0100
+++ b/src/HOL/Tools/Function/fun.ML	Mon Nov 23 15:05:59 2009 +0100
@@ -44,7 +44,7 @@
              ())
           end
           
-      val (fname, qs, gs, args, rhs) = split_def ctxt geq 
+      val (_, qs, gs, args, _) = split_def ctxt geq 
                                        
       val _ = if not (null gs) then err "Conditional equations" else ()
       val _ = map check_constr_pattern args
diff -r 26a4cb3a7eae -r cd8acf137c9c src/HOL/Tools/Function/function_core.ML
--- a/src/HOL/Tools/Function/function_core.ML	Mon Nov 23 13:45:16 2009 +0100
+++ b/src/HOL/Tools/Function/function_core.ML	Mon Nov 23 15:05:59 2009 +0100
@@ -97,8 +97,6 @@
 
 
 (* Theory dependencies. *)
-val Pair_inject = @{thm Product_Type.Pair_inject};
-
 val acc_induct_rule = @{thm accp_induct_rule};
 
 val ex1_implies_ex = @{thm FunDef.fundef_ex1_existence};
@@ -199,7 +197,7 @@
 
 fun mk_clause_info globals G f no cdata qglr tree RCs GIntro_thm RIntro_thms =
     let
-        val Globals {h, fvar, x, ...} = globals
+        val Globals {h, ...} = globals
 
         val ClauseContext { ctxt, qs, cqs, ags, ... } = cdata
         val cert = Thm.cterm_of (ProofContext.theory_of ctxt)
@@ -298,7 +296,7 @@
 (* Generates the replacement lemma in fully quantified form. *)
 fun mk_replacement_lemma thy h ih_elim clause =
     let
-        val ClauseInfo {cdata=ClauseContext {qs, lhs, rhs, cqs, ags, case_hyp, ...}, RCs, tree, ...} = clause
+        val ClauseInfo {cdata=ClauseContext {qs, lhs, cqs, ags, case_hyp, ...}, RCs, tree, ...} = clause
         local open Conv in
         val ih_conv = arg1_conv o arg_conv o arg_conv
         end
@@ -321,7 +319,7 @@
     end
 
 
-fun mk_uniqueness_clause thy globals f compat_store clausei clausej RLj =
+fun mk_uniqueness_clause thy globals compat_store clausei clausej RLj =
     let
         val Globals {h, y, x, fvar, ...} = globals
         val ClauseInfo {no=i, cdata=cctxi as ClauseContext {ctxt=ctxti, lhs=lhsi, case_hyp, ...}, ...} = clausei
@@ -355,10 +353,10 @@
 
 
 
-fun mk_uniqueness_case ctxt thy globals G f ihyp ih_intro G_cases compat_store clauses rep_lemmas clausei =
+fun mk_uniqueness_case thy globals G f ihyp ih_intro G_cases compat_store clauses rep_lemmas clausei =
     let
         val Globals {x, y, ranT, fvar, ...} = globals
-        val ClauseInfo {cdata = ClauseContext {lhs, rhs, qs, cqs, ags, case_hyp, ...}, lGI, RCs, ...} = clausei
+        val ClauseInfo {cdata = ClauseContext {lhs, rhs, cqs, ags, case_hyp, ...}, lGI, RCs, ...} = clausei
         val rhsC = Pattern.rewrite_term thy [(fvar, f)] [] rhs
 
         val ih_intro_case = full_simplify (HOL_basic_ss addsimps [case_hyp]) ih_intro
@@ -372,7 +370,7 @@
         val P = cterm_of thy (mk_eq (y, rhsC))
         val G_lhs_y = assume (cterm_of thy (HOLogic.mk_Trueprop (G $ lhs $ y)))
 
-        val unique_clauses = map2 (mk_uniqueness_clause thy globals f compat_store clausei) clauses rep_lemmas
+        val unique_clauses = map2 (mk_uniqueness_clause thy globals compat_store clausei) clauses rep_lemmas
 
         val uniqueness = G_cases
                            |> forall_elim (cterm_of thy lhs)
@@ -430,7 +428,7 @@
 
         val _ = trace_msg (K "Proving cases for unique existence...")
         val (ex1s, values) =
-            split_list (map (mk_uniqueness_case ctxt thy globals G f ihyp ih_intro G_elim compat_store clauses repLemmas) clauses)
+            split_list (map (mk_uniqueness_case thy globals G f ihyp ih_intro G_elim compat_store clauses repLemmas) clauses)
 
         val _ = trace_msg (K "Proving: Graph is a function")
         val graph_is_function = complete
@@ -523,7 +521,7 @@
         ((Binding.conceal (Binding.name fdefname), []), f_def)) lthy
   end
 
-fun define_recursion_relation Rname domT ranT fvar f qglrs clauses RCss lthy =
+fun define_recursion_relation Rname domT qglrs clauses RCss lthy =
   let
     val RT = domT --> domT --> boolT
     val (Rvar as (n, T)) = singleton (Variable.variant_frees lthy []) (Rname, RT)
@@ -700,8 +698,6 @@
         |> implies_intr D_dcl
         |> implies_intr D_subset
 
-  val subset_induct_all = fold_rev (forall_intr o cterm_of thy) [P, a, D] subset_induct_rule
-
   val simple_induct_rule =
       subset_induct_rule
         |> forall_intr (cterm_of thy D)
@@ -724,7 +720,7 @@
 fun mk_domain_intro ctxt (Globals {domT, ...}) R R_cases clause =
     let
       val thy = ProofContext.theory_of ctxt
-      val ClauseInfo {cdata = ClauseContext {qs, gs, lhs, rhs, cqs, ...},
+      val ClauseInfo {cdata = ClauseContext {gs, lhs, cqs, ...},
                       qglr = (oqs, _, _, _), ...} = clause
       val goal = HOLogic.mk_Trueprop (mk_acc domT R $ lhs)
                           |> fold_rev (curry Logic.mk_implies) gs
@@ -748,8 +744,8 @@
 
 fun mk_nest_term_case thy globals R' ihyp clause =
     let
-      val Globals {x, z, ...} = globals
-      val ClauseInfo {cdata = ClauseContext {qs,cqs,ags,lhs,rhs,case_hyp,...},tree,
+      val Globals {z, ...} = globals
+      val ClauseInfo {cdata = ClauseContext {qs, cqs, ags, lhs, case_hyp, ...},tree,
                       qglr=(oqs, _, _, _), ...} = clause
 
       val ih_case = full_simplify (HOL_basic_ss addsimps [case_hyp]) ihyp
@@ -868,7 +864,7 @@
 
       fun mk_trsimp clause psimp =
           let
-            val ClauseInfo {qglr = (oqs, _, _, _), cdata = ClauseContext {ctxt, cqs, qs, gs, lhs, rhs, ...}, ...} = clause
+            val ClauseInfo {qglr = (oqs, _, _, _), cdata = ClauseContext {ctxt, cqs, gs, lhs, rhs, ...}, ...} = clause
             val thy = ProofContext.theory_of ctxt
             val rhs_f = Pattern.rewrite_term thy [(fvar, f)] [] rhs
 
@@ -925,7 +921,7 @@
       val trees = map (Function_Ctx_Tree.inst_tree (ProofContext.theory_of lthy) fvar f) trees
 
       val ((R, RIntro_thmss, R_elim), lthy) =
-          PROFILE "def_rel" (define_recursion_relation (rel_name defname) domT ranT fvar f abstract_qglrs clauses RCss) lthy
+          PROFILE "def_rel" (define_recursion_relation (rel_name defname) domT abstract_qglrs clauses RCss) lthy
 
       val (_, lthy) =
           Local_Theory.abbrev Syntax.mode_default ((Binding.name (dom_name defname), NoSyn), mk_acc domT R) lthy
diff -r 26a4cb3a7eae -r cd8acf137c9c src/HOL/Tools/Function/function_lib.ML
--- a/src/HOL/Tools/Function/function_lib.ML	Mon Nov 23 13:45:16 2009 +0100
+++ b/src/HOL/Tools/Function/function_lib.ML	Mon Nov 23 15:05:59 2009 +0100
@@ -14,9 +14,6 @@
 fun fold_option f NONE y = y
   | fold_option f (SOME x) y = f x y;
 
-fun fold_map_option f NONE y = (NONE, y)
-  | fold_map_option f (SOME x) y = apfst SOME (f x y);
-
 (* Ex: "The variable" ^ plural " is" "s are" vs *)
 fun plural sg pl [x] = sg
   | plural sg pl _ = pl
@@ -53,7 +50,7 @@
 
 
 (* FIXME: similar to Variable.focus *)
-fun dest_all_all_ctx ctx (Const ("all", _) $ Abs (a as (n,T,b))) =
+fun dest_all_all_ctx ctx (Const ("all", _) $ Abs (n,T,b)) =
     let
       val [(n', _)] = Variable.variant_frees ctx [] [(n,T)]
       val (_, ctx') = ProofContext.add_fixes [(Binding.name n', SOME T, NoSyn)] ctx
diff -r 26a4cb3a7eae -r cd8acf137c9c src/HOL/Tools/Function/induction_schema.ML
--- a/src/HOL/Tools/Function/induction_schema.ML	Mon Nov 23 13:45:16 2009 +0100
+++ b/src/HOL/Tools/Function/induction_schema.ML	Mon Nov 23 15:05:59 2009 +0100
@@ -75,7 +75,7 @@
     let
       fun mk_branch concl =
           let
-            val (ctxt', ws, Cs, _ $ Pxs) = dest_hhf ctxt concl
+            val (_, ws, Cs, _ $ Pxs) = dest_hhf ctxt concl
             val (P, xs) = strip_comb Pxs
           in
             SchemeBranch { P=P, xs=map dest_Free xs, ws=ws, Cs=Cs }
@@ -103,7 +103,7 @@
 
             fun mk_rcinfo pr =
                 let
-                  val (ctxt'', Gvs, Gas, _ $ Phyp) = dest_hhf ctxt' pr
+                  val (_, Gvs, Gas, _ $ Phyp) = dest_hhf ctxt' pr
                   val (P', rcs) = strip_comb Phyp
                 in
                   (bidx P', Gvs, Gas, rcs)
@@ -151,7 +151,7 @@
        |> mk_forall_rename ("P", Pbool)
     end
 
-fun mk_wf ctxt R (IndScheme {T, ...}) =
+fun mk_wf R (IndScheme {T, ...}) =
     HOLogic.Trueprop $ (Const (@{const_name wf}, mk_relT T --> HOLogic.boolT) $ R)
 
 fun mk_ineqs R (IndScheme {T, cases, branches}) =
@@ -198,8 +198,6 @@
     end
 
 
-fun mk_hol_imp a b = HOLogic.imp $ a $ b
-
 fun mk_ind_goal thy branches =
     let
       fun brnch (SchemeBranch { P, xs, ws, Cs, ... }) =
@@ -256,7 +254,7 @@
             val (relevant_cases, ineqss') = filter (fn ((_, SchemeCase {bidx=bidx', ...}), _) => bidx' = bidx) (scases_idx ~~ ineqss)
                                             |> split_list
                            
-            fun prove_case (cidx, SchemeCase {qs, oqnames, gs, lhs, rs, ...}) ineq_press =
+            fun prove_case (cidx, SchemeCase {qs, gs, lhs, rs, ...}) ineq_press =
                 let
                   val case_hyps = map (assume o cert o HOLogic.mk_Trueprop o HOLogic.mk_eq) (fxs ~~ lhs)
                            
@@ -364,7 +362,7 @@
     val ineqss = mk_ineqs R scheme
                    |> map (map (pairself (assume o cert)))
     val complete = map_range (mk_completeness ctxt scheme #> cert #> assume) (length branches)
-    val wf_thm = mk_wf ctxt R scheme |> cert |> assume
+    val wf_thm = mk_wf R scheme |> cert |> assume
 
     val (descent, pres) = split_list (flat ineqss)
     val newgoals = complete @ pres @ wf_thm :: descent 
diff -r 26a4cb3a7eae -r cd8acf137c9c src/HOL/Tools/Function/lexicographic_order.ML
--- a/src/HOL/Tools/Function/lexicographic_order.ML	Mon Nov 23 13:45:16 2009 +0100
+++ b/src/HOL/Tools/Function/lexicographic_order.ML	Mon Nov 23 15:05:59 2009 +0100
@@ -75,10 +75,6 @@
       fold_rev Logic.all vars (Logic.list_implies (prems, concl))
     end
 
-fun prove thy solve_tac t =
-    cterm_of thy t |> Goal.init
-    |> SINGLE solve_tac |> the
-
 fun mk_cell (thy : theory) solve_tac (vars, prems, lhs, rhs) mfun =
     let
       val goals = cterm_of thy o mk_goal (vars, prems, mfun $ lhs, mfun $ rhs)
@@ -137,8 +133,6 @@
 
 (** Error reporting **)
 
-fun pr_table table = writeln (cat_lines (map (fn r => implode (map pr_cell r)) table))
-
 fun pr_goals ctxt st =
     Goal_Display.pretty_goals ctxt {total = true, main = false, maxgoals = Thm.nprems_of st} st
      |> Pretty.chunks
@@ -190,7 +184,7 @@
 fun lex_order_tac quiet ctxt solve_tac (st: thm) =
     let
       val thy = ProofContext.theory_of ctxt
-      val ((trueprop $ (wf $ rel)) :: tl) = prems_of st
+      val ((_ $ (_ $ rel)) :: tl) = prems_of st
 
       val (domT, _) = HOLogic.dest_prodT (HOLogic.dest_setT (fastype_of rel))
 
diff -r 26a4cb3a7eae -r cd8acf137c9c src/HOL/Tools/Function/mutual.ML
--- a/src/HOL/Tools/Function/mutual.ML	Mon Nov 23 13:45:16 2009 +0100
+++ b/src/HOL/Tools/Function/mutual.ML	Mon Nov 23 15:05:59 2009 +0100
@@ -28,8 +28,6 @@
 
 type qgar = string * (string * typ) list * term list * term list * term
 
-fun name_of_fqgar ((f, _, _, _, _): qgar) = f
-
 datatype mutual_part =
   MutualPart of 
    {
@@ -82,7 +80,6 @@
 fun analyze_eqs ctxt defname fs eqs =
     let
       val num = length fs
-        val fnames = map fst fs
         val fqgars = map (split_def ctxt) eqs
         val arity_of = map (fn (fname,_,_,args,_) => (fname, length args)) fqgars
                        |> AList.lookup (op =) #> the
@@ -108,7 +105,7 @@
         val ([fsum_var_name], _) = Variable.add_fixes [ defname ^ "_sum" ] ctxt
         val fsum_var = (fsum_var_name, fsum_type)
 
-        fun define (fvar as (n, T)) caTs resultT i =
+        fun define (fvar as (n, _)) caTs resultT i =
             let
                 val vars = map_index (fn (j,T) => Free ("x" ^ string_of_int j, T)) caTs (* FIXME: Bind xs properly *)
                 val i' = find_index (fn Ta => Ta = resultT) dresultTs + 1 
@@ -170,8 +167,8 @@
       val thy = ProofContext.theory_of ctxt
                 
       val oqnames = map fst pre_qs
-      val (qs, ctxt') = Variable.variant_fixes oqnames ctxt
-                        |>> map2 (fn (_, T) => fn n => Free (n, T)) pre_qs
+      val (qs, _) = Variable.variant_fixes oqnames ctxt
+        |>> map2 (fn (_, T) => fn n => Free (n, T)) pre_qs
                         
       fun inst t = subst_bounds (rev qs, t)
       val gs = map inst pre_gs
@@ -192,7 +189,7 @@
 
 fun recover_mutual_psimp all_orig_fdefs parts ctxt (fname, _, _, args, rhs) import (export : thm -> thm) sum_psimp_eq =
     let
-      val (MutualPart {f=SOME f, f_defthm=SOME f_def, ...}) = get_part fname parts
+      val (MutualPart {f=SOME f, ...}) = get_part fname parts
 
       val psimp = import sum_psimp_eq
       val (simp, restore_cond) = case cprems_of psimp of
@@ -223,7 +220,7 @@
     end
 
 
-fun mutual_induct_rules lthy induct all_f_defs (Mutual {n, ST, RST, parts, ...}) =
+fun mutual_induct_rules lthy induct all_f_defs (Mutual {n, ST, parts, ...}) =
     let
       val cert = cterm_of (ProofContext.theory_of lthy)
       val newPs = map2 (fn Pname => fn MutualPart {cargTs, ...} => 
@@ -266,8 +263,8 @@
 fun mk_partial_rules_mutual lthy inner_cont (m as Mutual {parts, fqgars, ...}) proof =
     let
       val result = inner_cont proof
-      val FunctionResult {fs=[f], G, R, cases, psimps, trsimps, simple_pinducts=[simple_pinduct],
-                        termination,domintros} = result
+      val FunctionResult {G, R, cases, psimps, trsimps, simple_pinducts=[simple_pinduct],
+        termination, domintros, ...} = result
                                                                                                                
       val (all_f_defs, fs) = map (fn MutualPart {f_defthm = SOME f_def, f = SOME f, cargTs, ...} =>
                                      (mk_applied_form lthy cargTs (symmetric f_def), f))
diff -r 26a4cb3a7eae -r cd8acf137c9c src/HOL/Tools/Function/pattern_split.ML
--- a/src/HOL/Tools/Function/pattern_split.ML	Mon Nov 23 13:45:16 2009 +0100
+++ b/src/HOL/Tools/Function/pattern_split.ML	Mon Nov 23 15:05:59 2009 +0100
@@ -50,9 +50,6 @@
 fun join ((vs1,sub1), (vs2,sub2)) = (merge (op aconv) (vs1,vs2), sub1 @ sub2)
 fun join_product (xs, ys) = map_product (curry join) xs ys
 
-fun join_list [] = []
-  | join_list xs = foldr1 (join_product) xs
-
 
 exception DISJ
 
diff -r 26a4cb3a7eae -r cd8acf137c9c src/HOL/Tools/Function/scnp_reconstruct.ML
--- a/src/HOL/Tools/Function/scnp_reconstruct.ML	Mon Nov 23 13:45:16 2009 +0100
+++ b/src/HOL/Tools/Function/scnp_reconstruct.ML	Mon Nov 23 15:05:59 2009 +0100
@@ -73,7 +73,7 @@
 
 val multiset_setup = Multiset_Setup.put o SOME
 
-fun undef x = error "undef"
+fun undef _ = error "undef"
 fun get_multiset_setup thy = Multiset_Setup.get thy
   |> the_default (Multiset
 { msetT = undef, mk_mset=undef,
@@ -153,14 +153,13 @@
 
 (* Reconstruction *)
 
-fun reconstruct_tac ctxt D cs (gp as GP (_, gs)) certificate =
+fun reconstruct_tac ctxt D cs (GP (_, gs)) certificate =
   let
     val thy = ProofContext.theory_of ctxt
     val Multiset
           { msetT, mk_mset,
-            mset_regroup_conv, mset_member_tac,
-            mset_nonempty_tac, mset_pwleq_tac, set_of_simps,
-            smsI', wmsI2'', wmsI1, reduction_pair=ms_rp } 
+            mset_regroup_conv, mset_pwleq_tac, set_of_simps,
+            smsI', wmsI2'', wmsI1, reduction_pair=ms_rp, ...} 
         = get_multiset_setup thy
 
     fun measure_fn p = nth (Termination.get_measures D p)
@@ -179,7 +178,7 @@
 
     fun prove_lev strict g =
       let
-        val G (p, q, el) = nth gs g
+        val G (p, q, _) = nth gs g
 
         fun less_proof strict (j, b) (i, a) =
           let
@@ -307,11 +306,10 @@
   | print_cell (SOME (False _)) = "-"
   | print_cell (NONE) = "?"
 
-fun print_error ctxt D = CALLS (fn (cs, i) =>
+fun print_error ctxt D = CALLS (fn (cs, _) =>
   let
     val np = get_num_points D
     val ms = map_range (get_measures D) np
-    val tys = map_range (get_types D) np
     fun index xs = (1 upto length xs) ~~ xs
     fun outp s t f xs = map (fn (x, y) => s ^ Int.toString x ^ t ^ f y ^ "\n") xs
     val ims = index (map index ms)
diff -r 26a4cb3a7eae -r cd8acf137c9c src/HOL/Tools/Function/scnp_solve.ML
--- a/src/HOL/Tools/Function/scnp_solve.ML	Mon Nov 23 13:45:16 2009 +0100
+++ b/src/HOL/Tools/Function/scnp_solve.ML	Mon Nov 23 15:05:59 2009 +0100
@@ -76,7 +76,7 @@
   Function_Common.PROFILE "sat_solving..." (SatSolver.invoke_solver (!solver)) x
 
 (* "Virtual constructors" for various propositional variables *)
-fun var_constrs (gp as GP (arities, gl)) =
+fun var_constrs (gp as GP (arities, _)) =
   let
     val n = Int.max (num_graphs gp, num_prog_pts gp)
     val k = fold Integer.max arities 1
diff -r 26a4cb3a7eae -r cd8acf137c9c src/HOL/Tools/Function/termination.ML
--- a/src/HOL/Tools/Function/termination.ML	Mon Nov 23 13:45:16 2009 +0100
+++ b/src/HOL/Tools/Function/termination.ML	Mon Nov 23 15:05:59 2009 +0100
@@ -148,7 +148,7 @@
     val cs = Function_Lib.dest_binop_list @{const_name Lattices.sup} rel
     fun collect_pats (Const (@{const_name Collect}, _) $ Abs (_, _, c)) =
       let
-        val (Const ("op &", _) $ (Const ("op =", _) $ _ $ (Const ("Pair", _) $ r $ l)) $ Gam)
+        val (Const ("op &", _) $ (Const ("op =", _) $ _ $ (Const ("Pair", _) $ r $ l)) $ _)
           = Term.strip_qnt_body "Ex" c
       in cons r o cons l end
   in
@@ -181,7 +181,6 @@
 
 fun dest_call D (Const (@{const_name Collect}, _) $ Abs (_, _, c)) =
   let
-    val n = get_num_points D
     val (sk, _, _, _, _) = D
     val vs = Term.strip_qnt_vars "Ex" c
 
@@ -196,7 +195,7 @@
   | dest_call D t = error "dest_call"
 
 
-fun derive_desc_aux thy tac c (vs, p, l', q, r', Gam) m1 m2 D =
+fun derive_desc_aux thy tac c (vs, _, l', _, r', Gam) m1 m2 D =
   case get_descent D c m1 m2 of
     SOME _ => D
   | NONE => let
@@ -225,7 +224,7 @@
 
 (* all descents in one go *)
 fun derive_descents thy tac c D =
-  let val cdesc as (vs, p, l', q, r', Gam) = dest_call D c
+  let val cdesc as (_, p, _, q, _, _) = dest_call D c
   in fold_product (derive_desc_aux thy tac c cdesc)
        (get_measures D p) (get_measures D q) D
   end
@@ -280,7 +279,7 @@
     let
       val thy = ProofContext.theory_of ctxt
       val cert = cterm_of (theory_of_thm st)
-      val ((trueprop $ (wf $ rel)) :: ineqs) = prems_of st
+      val ((_ $ (_ $ rel)) :: ineqs) = prems_of st
 
       fun mk_compr ineq =
           let