# HG changeset patch
# User wenzelm
# Date 1632080234 -7200
# Node ID 54b2e5f771daf27f1c23c3986b60cd8347e8add6
# Parent  3360ea6b659dbb03eb7dce90b0bd052dc798199a
clarified signature -- prefer antiquotations (with subtle change of exception content);

diff -r 3360ea6b659d -r 54b2e5f771da src/FOL/fologic.ML
--- a/src/FOL/fologic.ML	Sun Sep 19 21:35:51 2021 +0200
+++ b/src/FOL/fologic.ML	Sun Sep 19 21:37:14 2021 +0200
@@ -6,14 +6,8 @@
 
 signature FOLOGIC =
 sig
-  val oT: typ
   val mk_Trueprop: term -> term
   val dest_Trueprop: term -> term
-  val not: term
-  val conj: term
-  val disj: term
-  val imp: term
-  val iff: term
   val mk_conj: term * term -> term
   val mk_disj: term * term -> term
   val mk_imp: term * term -> term
@@ -28,52 +22,32 @@
   val eq_const: typ -> term
   val mk_eq: term * term -> term
   val dest_eq: term -> term * term
-  val mk_binop: string -> term * term -> term
-  val mk_binrel: string -> term * term -> term
-  val dest_bin: string -> typ -> term -> term * term
 end;
 
 
 structure FOLogic: FOLOGIC =
 struct
 
-val oT = \<^Type>\<open>o\<close>;
-
-val Trueprop = \<^Const>\<open>Trueprop\<close>;
-
-fun mk_Trueprop P = Trueprop $ P;
+fun mk_Trueprop P = \<^Const>\<open>Trueprop for P\<close>;
 
-fun dest_Trueprop \<^Const_>\<open>Trueprop for P\<close> = P
-  | dest_Trueprop t = raise TERM ("dest_Trueprop", [t]);
-
-
-(* Logical constants *)
+val dest_Trueprop = \<^Const_fn>\<open>Trueprop for P => P\<close>;
 
-val not = \<^Const>\<open>Not\<close>;
-val conj = \<^Const>\<open>conj\<close>;
-val disj = \<^Const>\<open>disj\<close>;
-val imp = \<^Const>\<open>imp\<close>;
-val iff = \<^Const>\<open>iff\<close>;
+fun mk_conj (t1, t2) = \<^Const>\<open>conj for t1 t2\<close>
+and mk_disj (t1, t2) = \<^Const>\<open>disj for t1 t2\<close>
+and mk_imp (t1, t2) = \<^Const>\<open>imp for t1 t2\<close>
+and mk_iff (t1, t2) = \<^Const>\<open>iff for t1 t2\<close>;
 
-fun mk_conj (t1, t2) = conj $ t1 $ t2
-and mk_disj (t1, t2) = disj $ t1 $ t2
-and mk_imp (t1, t2) = imp $ t1 $ t2
-and mk_iff (t1, t2) = iff $ t1 $ t2;
-
-fun dest_imp \<^Const_>\<open>imp for A B\<close> = (A, B)
-  | dest_imp  t = raise TERM ("dest_imp", [t]);
+val dest_imp = \<^Const_fn>\<open>imp for A B => \<open>(A, B)\<close>\<close>;
 
 fun dest_conj \<^Const_>\<open>conj for t t'\<close> = t :: dest_conj t'
   | dest_conj t = [t];
 
-fun dest_iff \<^Const_>\<open>iff for A B\<close> = (A, B)
-  | dest_iff  t = raise TERM ("dest_iff", [t]);
+val dest_iff = \<^Const_fn>\<open>iff for A B => \<open>(A, B)\<close>\<close>;
 
 fun eq_const T = \<^Const>\<open>eq T\<close>;
 fun mk_eq (t, u) = eq_const (fastype_of t) $ t $ u;
 
-fun dest_eq \<^Const_>\<open>eq _ for lhs rhs\<close> = (lhs, rhs)
-  | dest_eq t = raise TERM ("dest_eq", [t])
+val dest_eq = \<^Const_fn>\<open>eq _ for lhs rhs => \<open>(lhs, rhs)\<close>\<close>;
 
 fun all_const T = \<^Const>\<open>All T\<close>;
 fun mk_all (Free (x, T), P) = all_const T $ absfree (x, T) P;
@@ -81,22 +55,4 @@
 fun exists_const T = \<^Const>\<open>Ex T\<close>;
 fun mk_exists (Free (x, T), P) = exists_const T $ absfree (x, T) P;
 
-
-(* binary operations and relations *)
-
-fun mk_binop c (t, u) =
-  let val T = fastype_of t in
-    Const (c, [T, T] ---> T) $ t $ u
-  end;
-
-fun mk_binrel c (t, u) =
-  let val T = fastype_of t in
-    Const (c, [T, T] ---> oT) $ t $ u
-  end;
-
-fun dest_bin c T (tm as Const (c', Type ("fun", [T', _])) $ t $ u) =
-      if c = c' andalso T = T' then (t, u)
-      else raise TERM ("dest_bin " ^ c, [tm])
-  | dest_bin c _ tm = raise TERM ("dest_bin " ^ c, [tm]);
-
 end;
diff -r 3360ea6b659d -r 54b2e5f771da src/FOL/simpdata.ML
--- a/src/FOL/simpdata.ML	Sun Sep 19 21:35:51 2021 +0200
+++ b/src/FOL/simpdata.ML	Sun Sep 19 21:37:14 2021 +0200
@@ -63,8 +63,8 @@
     | dest_conj _ = NONE
   fun dest_imp \<^Const_>\<open>imp for s t\<close> = SOME (s, t)
     | dest_imp _ = NONE
-  val conj = FOLogic.conj
-  val imp  = FOLogic.imp
+  val conj = \<^Const>\<open>conj\<close>
+  val imp  = \<^Const>\<open>imp\<close>
   (*rules*)
   val iff_reflection = @{thm iff_reflection}
   val iffI = @{thm iffI}
diff -r 3360ea6b659d -r 54b2e5f771da src/ZF/Tools/cartprod.ML
--- a/src/ZF/Tools/cartprod.ML	Sun Sep 19 21:35:51 2021 +0200
+++ b/src/ZF/Tools/cartprod.ML	Sun Sep 19 21:37:14 2021 +0200
@@ -70,24 +70,22 @@
 fun pseudo_type (t $ A $ Abs(_,_,B)) = 
       if t = Pr.sigma
       then mk_prod(pseudo_type A, pseudo_type B)
-      else \<^typ>\<open>i\<close>
-  | pseudo_type _ = \<^typ>\<open>i\<close>;
+      else \<^Type>\<open>i\<close>
+  | pseudo_type _ = \<^Type>\<open>i\<close>;
 
 (*Maps the type T1*...*Tn to [T1,...,Tn], however nested*)
 fun factors (Type("*", [T1, T2])) = factors T1 @ factors T2
   | factors T                     = [T];
 
 (*Make a well-typed instance of "split"*)
-fun split_const T = Const(Pr.split_name, 
-                          [[Ind_Syntax.iT, Ind_Syntax.iT]--->T, 
-                           Ind_Syntax.iT] ---> T);
+fun split_const T = Const(Pr.split_name, [[\<^Type>\<open>i\<close>, \<^Type>\<open>i\<close>]--->T, \<^Type>\<open>i\<close>] ---> T);
 
 (*In ap_split S T u, term u expects separate arguments for the factors of S,
   with result type T.  The call creates a new term expecting one argument
   of type S.*)
 fun ap_split (Type("*", [T1,T2])) T3 u   = 
        split_const T3 $ 
-       Abs("v", Ind_Syntax.iT, (*Not T1, as it involves pseudo-product types*)
+       Abs("v", \<^Type>\<open>i\<close>, (*Not T1, as it involves pseudo-product types*)
            ap_split T2 T3
            ((ap_split T1 (factors T2 ---> T3) (incr_boundvars 1 u)) $ 
             Bound 0))
@@ -109,7 +107,7 @@
       in
         remove_split ctxt
           (Drule.instantiate_normalize (TVars.empty,
-            Vars.make [((v, Ind_Syntax.iT-->T2), Thm.cterm_of ctxt newt)]) rl)
+            Vars.make [((v, \<^Type>\<open>i\<close> --> T2), Thm.cterm_of ctxt newt)]) rl)
       end
   | split_rule_var _ (t,T,rl) = rl;
 
diff -r 3360ea6b659d -r 54b2e5f771da src/ZF/Tools/datatype_package.ML
--- a/src/ZF/Tools/datatype_package.ML	Sun Sep 19 21:35:51 2021 +0200
+++ b/src/ZF/Tools/datatype_package.ML	Sun Sep 19 21:37:14 2021 +0200
@@ -115,10 +115,10 @@
 
   (*Combine split terms using case; yields the case operator for one part*)
   fun call_case case_list =
-    let fun call_f (free,[]) = Abs("null", \<^typ>\<open>i\<close>, free)
+    let fun call_f (free,[]) = Abs("null", \<^Type>\<open>i\<close>, free)
           | call_f (free,args) =
                 CP.ap_split (foldr1 CP.mk_prod (map (#2 o dest_Free) args))
-                            \<^typ>\<open>i\<close>
+                            \<^Type>\<open>i\<close>
                             free
     in  Balanced_Tree.make (fn (t1, t2) => Su.elim $ t1 $ t2) (map call_f case_list)  end;
 
@@ -162,7 +162,7 @@
       Non-identifiers (e.g. infixes) get a name of the form f_op_nnn. **)
 
   (*a recursive call for x is the application rec`x  *)
-  val rec_call = \<^Const>\<open>apply\<close> $ Free ("rec", \<^typ>\<open>i\<close>);
+  val rec_call = \<^Const>\<open>apply\<close> $ Free ("rec", \<^Type>\<open>i\<close>);
 
   (*look back down the "case args" (which have been reversed) to
     determine the de Bruijn index*)
@@ -199,7 +199,7 @@
   (*Add an argument position for each occurrence of a recursive set.
     Strictly speaking, the recursive arguments are the LAST of the function
     variable, but they all have type "i" anyway*)
-  fun add_rec_args args' T = (map (fn _ => \<^typ>\<open>i\<close>) args') ---> T
+  fun add_rec_args args' T = (map (fn _ => \<^Type>\<open>i\<close>) args') ---> T
 
   (*Plug in the function variable type needed for the recursor
     as well as the new arguments (recursive calls)*)
@@ -232,7 +232,7 @@
       Misc_Legacy.mk_defpair
         (recursor_tm,
          \<^Const>\<open>Univ.Vrecursor\<close> $
-           absfree ("rec", \<^typ>\<open>i\<close>) (list_comb (case_const, recursor_cases)));
+           absfree ("rec", \<^Type>\<open>i\<close>) (list_comb (case_const, recursor_cases)));
 
   (* Build the new theory *)
 
@@ -412,7 +412,7 @@
   let
     val ctxt = Proof_Context.init_global thy;
     fun read_is strs =
-      map (Syntax.parse_term ctxt #> Type.constraint \<^typ>\<open>i\<close>) strs
+      map (Syntax.parse_term ctxt #> Type.constraint \<^Type>\<open>i\<close>) strs
       |> Syntax.check_terms ctxt;
 
     val rec_tms = read_is srec_tms;
diff -r 3360ea6b659d -r 54b2e5f771da src/ZF/Tools/inductive_package.ML
--- a/src/ZF/Tools/inductive_package.ML	Sun Sep 19 21:35:51 2021 +0200
+++ b/src/ZF/Tools/inductive_package.ML	Sun Sep 19 21:37:14 2021 +0200
@@ -108,14 +108,14 @@
     let val prems = map dest_tprop (Logic.strip_imp_prems intr)
         val dummy = List.app (fn rec_hd => List.app (Ind_Syntax.chk_prem rec_hd) prems) rec_hds
         val exfrees = subtract (op =) rec_params (Misc_Legacy.term_frees intr)
-        val zeq = FOLogic.mk_eq (Free(z', Ind_Syntax.iT), #1 (Ind_Syntax.rule_concl intr))
+        val zeq = FOLogic.mk_eq (Free(z', \<^Type>\<open>i\<close>), #1 (Ind_Syntax.rule_concl intr))
     in List.foldr FOLogic.mk_exists
              (Balanced_Tree.make FOLogic.mk_conj (zeq::prems)) exfrees
     end;
 
   (*The Part(A,h) terms -- compose injections to make h*)
-  fun mk_Part (Bound 0) = Free(X', Ind_Syntax.iT) (*no mutual rec, no Part needed*)
-    | mk_Part h = \<^Const>\<open>Part\<close> $ Free(X', Ind_Syntax.iT) $ Abs (w', Ind_Syntax.iT, h);
+  fun mk_Part (Bound 0) = Free(X', \<^Type>\<open>i\<close>) (*no mutual rec, no Part needed*)
+    | mk_Part h = \<^Const>\<open>Part\<close> $ Free(X', \<^Type>\<open>i\<close>) $ Abs (w', \<^Type>\<open>i\<close>, h);
 
   (*Access to balanced disjoint sums via injections*)
   val parts = map mk_Part
@@ -126,7 +126,7 @@
   val part_intrs = map (subst_free (rec_tms ~~ parts) o fp_part) intr_tms;
 
   val fp_abs =
-    absfree (X', Ind_Syntax.iT)
+    absfree (X', \<^Type>\<open>i\<close>)
         (Ind_Syntax.mk_Collect (z', dom_sum,
             Balanced_Tree.make FOLogic.mk_disj part_intrs));
 
@@ -159,7 +159,7 @@
          (case parts of
              [_] => []                        (*no mutual recursion*)
            | _ => rec_tms ~~          (*define the sets as Parts*)
-                  map (subst_atomic [(Free (X', Ind_Syntax.iT), big_rec_tm)]) parts));
+                  map (subst_atomic [(Free (X', \<^Type>\<open>i\<close>), big_rec_tm)]) parts));
 
   (*tracing: print the fixedpoint definition*)
   val dummy = if !Ind_Syntax.trace then
@@ -323,7 +323,7 @@
        | ind_tac ctxt (prem::prems) i =
              DEPTH_SOLVE_1 (ares_tac ctxt [prem, @{thm refl}] i) THEN ind_tac ctxt prems (i-1);
 
-     val pred = Free(pred_name, Ind_Syntax.iT --> FOLogic.oT);
+     val pred = Free(pred_name, \<^Type>\<open>i\<close> --> \<^Type>\<open>o\<close>);
 
      val ind_prems = map (induct_prem (map (rpair pred) rec_tms))
                          intr_tms;
@@ -387,12 +387,12 @@
      fun mk_predpair rec_tm =
        let val rec_name = (#1 o dest_Const o head_of) rec_tm
            val pfree = Free(pred_name ^ "_" ^ Long_Name.base_name rec_name,
-                            elem_factors ---> FOLogic.oT)
+                            elem_factors ---> \<^Type>\<open>o\<close>)
            val qconcl =
              List.foldr FOLogic.mk_all
-               (FOLogic.imp $ \<^Const>\<open>mem for elem_tuple rec_tm\<close>
+               (\<^Const>\<open>imp\<close> $ \<^Const>\<open>mem for elem_tuple rec_tm\<close>
                       $ (list_comb (pfree, elem_frees))) elem_frees
-       in  (CP.ap_split elem_type FOLogic.oT pfree,
+       in  (CP.ap_split elem_type \<^Type>\<open>o\<close> pfree,
             qconcl)
        end;
 
@@ -400,14 +400,14 @@
 
      (*Used to form simultaneous induction lemma*)
      fun mk_rec_imp (rec_tm,pred) =
-         FOLogic.imp $ \<^Const>\<open>mem for \<open>Bound 0\<close> rec_tm\<close> $ (pred $ Bound 0);
+         \<^Const>\<open>imp\<close> $ \<^Const>\<open>mem for \<open>Bound 0\<close> rec_tm\<close> $ (pred $ Bound 0);
 
      (*To instantiate the main induction rule*)
      val induct_concl =
          FOLogic.mk_Trueprop
            (Ind_Syntax.mk_all_imp
             (big_rec_tm,
-             Abs("z", Ind_Syntax.iT,
+             Abs("z", \<^Type>\<open>i\<close>,
                  Balanced_Tree.make FOLogic.mk_conj
                  (ListPair.map mk_rec_imp (rec_tms, preds)))))
      and mutual_induct_concl =
@@ -515,7 +515,7 @@
 
      val induct0 =
        CP.split_rule_var ctxt4
-        (pred_var, elem_type-->FOLogic.oT, induct0)
+        (pred_var, elem_type --> \<^Type>\<open>o\<close>, induct0)
        |> Drule.export_without_context
      and mutual_induct = CP.remove_split ctxt4 mutual_induct_fsplit
 
@@ -564,7 +564,7 @@
     (raw_monos, raw_con_defs, raw_type_intrs, raw_type_elims) thy =
   let
     val ctxt = Proof_Context.init_global thy;
-    val read_terms = map (Syntax.parse_term ctxt #> Type.constraint Ind_Syntax.iT)
+    val read_terms = map (Syntax.parse_term ctxt #> Type.constraint \<^Type>\<open>i\<close>)
       #> Syntax.check_terms ctxt;
 
     val intr_atts = map (map (Attrib.attribute_cmd ctxt) o snd) intr_srcs;
diff -r 3360ea6b659d -r 54b2e5f771da src/ZF/Tools/primrec_package.ML
--- a/src/ZF/Tools/primrec_package.ML	Sun Sep 19 21:35:51 2021 +0200
+++ b/src/ZF/Tools/primrec_package.ML	Sun Sep 19 21:37:14 2021 +0200
@@ -106,7 +106,7 @@
     and recursor_pairs = map (dest_eqn o Thm.concl_of) rec_rewrites
 
     fun absterm (Free x, body) = absfree x body
-      | absterm (t, body) = Abs("rec", Ind_Syntax.iT, abstract_over (t, body))
+      | absterm (t, body) = Abs("rec", \<^Type>\<open>i\<close>, abstract_over (t, body))
 
     (*Translate rec equations into function arguments suitable for recursor.
       Missing cases are replaced by 0 and all cases are put into order.*)
@@ -140,7 +140,7 @@
     (*the recursive argument*)
     val rec_arg =
       Free (singleton (Name.variant_list (map #1 (ls@rs))) (Long_Name.base_name big_rec_name),
-        Ind_Syntax.iT)
+        \<^Type>\<open>i\<close>)
 
     val def_tm = Logic.mk_equals
                     (subst_bound (rec_arg, fabs),
diff -r 3360ea6b659d -r 54b2e5f771da src/ZF/arith_data.ML
--- a/src/ZF/arith_data.ML	Sun Sep 19 21:35:51 2021 +0200
+++ b/src/ZF/arith_data.ML	Sun Sep 19 21:37:14 2021 +0200
@@ -22,8 +22,6 @@
 structure ArithData: ARITH_DATA =
 struct
 
-val iT = Ind_Syntax.iT;
-
 val zero = \<^Const>\<open>zero\<close>;
 val succ = \<^Const>\<open>succ\<close>;
 fun mk_succ t = succ $ t;
@@ -49,8 +47,9 @@
 
 (*Use <-> or = depending on the type of t*)
 fun mk_eq_iff(t,u) =
-  if fastype_of t = iT then FOLogic.mk_eq(t,u)
-                       else FOLogic.mk_iff(t,u);
+  if fastype_of t = \<^Type>\<open>i\<close>
+  then \<^Const>\<open>IFOL.eq \<open>\<^Type>\<open>i\<close>\<close> for t u\<close>
+  else \<^Const>\<open>IFOL.iff for t u\<close>;
 
 (*We remove equality assumptions because they confuse the simplifier and
   because only type-checking assumptions are necessary.*)
@@ -79,12 +78,10 @@
   | mk_prod (t :: ts) = if t = one then mk_prod ts
                         else mk_times (t, mk_prod ts);
 
-val dest_times = FOLogic.dest_bin \<^const_name>\<open>Arith.mult\<close> iT;
-
-fun dest_prod t =
-      let val (t,u) = dest_times t
-      in  dest_prod t @ dest_prod u  end
-      handle TERM _ => [t];
+fun dest_prod tm =
+  let val (t,u) = \<^Const_fn>\<open>Arith.mult for t u => \<open>(t, u)\<close>\<close> tm
+  in  dest_prod t @ dest_prod u  end
+  handle TERM _ => [tm];
 
 (*Dummy version: the only arguments are 0 and 1*)
 fun mk_coeff (0, t) = zero
@@ -168,7 +165,7 @@
   open CancelNumeralsCommon
   val prove_conv = prove_conv "natless_cancel_numerals"
   fun mk_bal (t, u) = \<^Const>\<open>Ordinal.lt for t u\<close>
-  val dest_bal = FOLogic.dest_bin \<^const_name>\<open>Ordinal.lt\<close> iT
+  val dest_bal = \<^Const_fn>\<open>Ordinal.lt for t u => \<open>(t, u)\<close>\<close>
   val bal_add1 = @{thm less_add_iff [THEN iff_trans]}
   val bal_add2 = @{thm less_add_iff [THEN iff_trans]}
   fun trans_tac ctxt = gen_trans_tac ctxt @{thm iff_trans}
@@ -181,7 +178,7 @@
   open CancelNumeralsCommon
   val prove_conv = prove_conv "natdiff_cancel_numerals"
   fun mk_bal (t, u) = \<^Const>\<open>Arith.diff for t u\<close>
-  val dest_bal = FOLogic.dest_bin \<^const_name>\<open>Arith.diff\<close> iT
+  val dest_bal = \<^Const_fn>\<open>Arith.diff for t u => \<open>(t, u)\<close>\<close>
   val bal_add1 = @{thm diff_add_eq [THEN trans]}
   val bal_add2 = @{thm diff_add_eq [THEN trans]}
   fun trans_tac ctxt = gen_trans_tac ctxt @{thm trans}
diff -r 3360ea6b659d -r 54b2e5f771da src/ZF/ind_syntax.ML
--- a/src/ZF/ind_syntax.ML	Sun Sep 19 21:35:51 2021 +0200
+++ b/src/ZF/ind_syntax.ML	Sun Sep 19 21:37:14 2021 +0200
@@ -18,14 +18,12 @@
 
 (** Abstract syntax definitions for ZF **)
 
-val iT = \<^Type>\<open>i\<close>;
-
 (*Creates All(%v.v:A --> P(v)) rather than Ball(A,P) *)
 fun mk_all_imp (A,P) =
-    FOLogic.all_const iT $
-      Abs("v", iT, FOLogic.imp $ \<^Const>\<open>mem for \<open>Bound 0\<close> A\<close> $ Term.betapply(P, Bound 0));
+    FOLogic.all_const \<^Type>\<open>i\<close> $
+      Abs("v", \<^Type>\<open>i\<close>, \<^Const>\<open>imp\<close> $ \<^Const>\<open>mem for \<open>Bound 0\<close> A\<close> $ Term.betapply(P, Bound 0));
 
-fun mk_Collect (a, D, t) = \<^Const>\<open>Collect for D\<close> $ absfree (a, iT) t;
+fun mk_Collect (a, D, t) = \<^Const>\<open>Collect for D\<close> $ absfree (a, \<^Type>\<open>i\<close>) t;
 
 (*simple error-checking in the premises of an inductive definition*)
 fun chk_prem rec_hd \<^Const_>\<open>conj for _ _\<close> =
@@ -64,10 +62,10 @@
 
 (*read a constructor specification*)
 fun read_construct ctxt (id: string, sprems, syn: mixfix) =
-    let val prems = map (Syntax.parse_term ctxt #> Type.constraint FOLogic.oT) sprems
+    let val prems = map (Syntax.parse_term ctxt #> Type.constraint \<^Type>\<open>o\<close>) sprems
           |> Syntax.check_terms ctxt
         val args = map (#1 o dest_mem) prems
-        val T = (map (#2 o dest_Free) args) ---> iT
+        val T = (map (#2 o dest_Free) args) ---> \<^Type>\<open>i\<close>
                 handle TERM _ => error
                     "Bad variable in constructor specification"
     in ((id,T,syn), id, args, prems) end;
@@ -91,7 +89,7 @@
 (*Make a datatype's domain: form the union of its set parameters*)
 fun union_params (rec_tm, cs) =
   let val (_,args) = strip_comb rec_tm
-      fun is_ind arg = (type_of arg = iT)
+      fun is_ind arg = (type_of arg = \<^Type>\<open>i\<close>)
   in  case filter is_ind (args @ cs) of
          [] => \<^Const>\<open>zero\<close>
        | u_args => Balanced_Tree.make mk_Un u_args
diff -r 3360ea6b659d -r 54b2e5f771da src/ZF/int_arith.ML
--- a/src/ZF/int_arith.ML	Sun Sep 19 21:35:51 2021 +0200
+++ b/src/ZF/int_arith.ML	Sun Sep 19 21:37:14 2021 +0200
@@ -82,12 +82,10 @@
   | mk_prod (t :: ts) = if t = one then mk_prod ts
                         else mk_times (t, mk_prod ts);
 
-val dest_times = FOLogic.dest_bin \<^const_name>\<open>zmult\<close> \<^typ>\<open>i\<close>;
-
-fun dest_prod t =
-      let val (t,u) = dest_times t
-      in  dest_prod t @ dest_prod u  end
-      handle TERM _ => [t];
+fun dest_prod tm =
+  let val (t,u) = \<^Const_fn>\<open>zmult for t u => \<open>(t, u)\<close>\<close> tm
+  in  dest_prod t @ dest_prod u  end
+  handle TERM _ => [tm];
 
 (*DON'T do the obvious simplifications; that would create special cases*)
 fun mk_coeff (k, t) = mk_times (mk_numeral k, t);
@@ -192,7 +190,7 @@
  (open CancelNumeralsCommon
   val prove_conv = ArithData.prove_conv "intless_cancel_numerals"
   fun mk_bal (t, u) = \<^Const>\<open>zless for t u\<close>
-  val dest_bal = FOLogic.dest_bin \<^const_name>\<open>zless\<close> \<^typ>\<open>i\<close>
+  val dest_bal = \<^Const_fn>\<open>zless for t u => \<open>(t, u)\<close>\<close>
   val bal_add1 = @{thm less_add_iff1} RS @{thm iff_trans}
   val bal_add2 = @{thm less_add_iff2} RS @{thm iff_trans}
 );
@@ -201,7 +199,7 @@
  (open CancelNumeralsCommon
   val prove_conv = ArithData.prove_conv "intle_cancel_numerals"
   fun mk_bal (t, u) = \<^Const>\<open>zle for t u\<close>
-  val dest_bal = FOLogic.dest_bin \<^const_name>\<open>zle\<close> \<^typ>\<open>i\<close>
+  val dest_bal = \<^Const_fn>\<open>zle for t u => \<open>(t, u)\<close>\<close>
   val bal_add1 = @{thm le_add_iff1} RS @{thm iff_trans}
   val bal_add2 = @{thm le_add_iff2} RS @{thm iff_trans}
 );