# HG changeset patch
# User wenzelm
# Date 1633169054 -7200
# Node ID 4cdc5e946c997387ef1b618a20de0fb1b00232fc
# Parent  71dfb835025d60a04e7b6dcbea3f63cf5e91cd9f
proper term operation Term.dest_abs;

diff -r 71dfb835025d -r 4cdc5e946c99 src/FOLP/simp.ML
--- a/src/FOLP/simp.ML	Sat Oct 02 11:56:11 2021 +0200
+++ b/src/FOLP/simp.ML	Sat Oct 02 12:04:14 2021 +0200
@@ -366,7 +366,7 @@
 (*Replace parameters by Free variables in P*)
 fun variants_abs ([],P) = P
   | variants_abs ((a,T)::aTs, P) =
-      variants_abs (aTs, #2 (Syntax_Trans.variant_abs(a,T,P)));
+      variants_abs (aTs, #2 (Term.dest_abs(a,T,P)));
 
 (*Select subgoal i from proof state; substitute parameters, for printing*)
 fun prepare_goal i st =
diff -r 71dfb835025d -r 4cdc5e946c99 src/HOL/Decision_Procs/Cooper.thy
--- a/src/HOL/Decision_Procs/Cooper.thy	Sat Oct 02 11:56:11 2021 +0200
+++ b/src/HOL/Decision_Procs/Cooper.thy	Sat Oct 02 12:04:14 2021 +0200
@@ -2429,12 +2429,12 @@
       @{code Not} (fm_of_term ps vs t')
   | fm_of_term ps vs \<^Const_>\<open>Ex _ for \<open>Abs (xn, xT, p)\<close>\<close> =
       let
-        val (xn', p') = Syntax_Trans.variant_abs (xn, xT, p);  (* FIXME !? *)
+        val (xn', p') = Term.dest_abs (xn, xT, p);
         val vs' = (Free (xn', xT), 0) :: map (fn (v, n) => (v, n + 1)) vs;
       in @{code E} (fm_of_term ps vs' p) end
   | fm_of_term ps vs \<^Const_>\<open>All _ for \<open>Abs (xn, xT, p)\<close>\<close> =
       let
-        val (xn', p') = Syntax_Trans.variant_abs (xn, xT, p);  (* FIXME !? *)
+        val (xn', p') = Term.dest_abs (xn, xT, p);
         val vs' = (Free (xn', xT), 0) :: map (fn (v, n) => (v, n + 1)) vs;
       in @{code A} (fm_of_term ps vs' p) end
   | fm_of_term ps vs t = error ("fm_of_term : unknown term " ^ Syntax.string_of_term \<^context> t);
@@ -2505,7 +2505,7 @@
     | f $ a =>
         if is_ty t orelse is_op t then term_bools (term_bools acc f) a
         else insert (op aconv) t acc
-    | Abs p => term_bools acc (snd (Syntax_Trans.variant_abs p))  (* FIXME !? *)
+    | Abs p => term_bools acc (snd (Term.dest_abs p))
     | _ => if is_ty t orelse is_op t then acc else insert (op aconv) t acc)
   end;
 
diff -r 71dfb835025d -r 4cdc5e946c99 src/HOL/Decision_Procs/Parametric_Ferrante_Rackoff.thy
--- a/src/HOL/Decision_Procs/Parametric_Ferrante_Rackoff.thy	Sat Oct 02 11:56:11 2021 +0200
+++ b/src/HOL/Decision_Procs/Parametric_Ferrante_Rackoff.thy	Sat Oct 02 12:04:14 2021 +0200
@@ -3975,12 +3975,10 @@
   | fm_of_term fs ps \<^Const_>\<open>less_eq _ for p q\<close> =
       @{code Le} (@{code Sub} (tm_of_term fs ps p, tm_of_term fs ps q))
   | fm_of_term fs ps (\<^Const_>\<open>Ex _\<close> $ Abs (abs as (_, xT, _))) =
-      let
-        val (xn', p') = Syntax_Trans.variant_abs abs;  (* FIXME !? *)
+      let val (xn', p') = Term.dest_abs abs
       in @{code E} (fm_of_term (Free (xn', xT) :: fs) ps p') end
   | fm_of_term fs ps (\<^Const_>\<open>All _\<close> $ Abs (abs as (_, xT, _))) =
-      let
-        val (xn', p') = Syntax_Trans.variant_abs abs;  (* FIXME !? *)
+      let val (xn', p') = Term.dest_abs abs
       in @{code A} (fm_of_term (Free (xn', xT) :: fs) ps p') end
   | fm_of_term fs ps _ = error "fm_of_term";
 
diff -r 71dfb835025d -r 4cdc5e946c99 src/HOL/Tools/Qelim/cooper.ML
--- a/src/HOL/Tools/Qelim/cooper.ML	Sat Oct 02 11:56:11 2021 +0200
+++ b/src/HOL/Tools/Qelim/cooper.ML	Sat Oct 02 12:04:14 2021 +0200
@@ -599,13 +599,12 @@
               else insert (op aconv) t
     | f $ a => if skip orelse is_op f then add_bools a o add_bools f
               else insert (op aconv) t
-    | Abs p => add_bools (snd (Syntax_Trans.variant_abs p))  (* FIXME !? *)
+    | Abs p => add_bools (snd (Term.dest_abs p))
     | _ => if skip orelse is_op t then I else insert (op aconv) t
   end;
 
 fun descend vs (abs as (_, xT, _)) =
-  let
-    val (xn', p') = Syntax_Trans.variant_abs abs;  (* FIXME !? *)
+  let val (xn', p') = Term.dest_abs abs
   in ((xn', xT) :: vs, p') end;
 
 local structure Proc = Cooper_Procedure in
diff -r 71dfb835025d -r 4cdc5e946c99 src/HOL/Tools/reification.ML
--- a/src/HOL/Tools/reification.ML	Sat Oct 02 11:56:11 2021 +0200
+++ b/src/HOL/Tools/reification.ML	Sat Oct 02 12:04:14 2021 +0200
@@ -139,7 +139,7 @@
         Abs (_, xT, ta) =>
           let
             val ([raw_xn], ctxt') = Variable.variant_fixes ["x"] ctxt;
-            val (xn, ta) = Syntax_Trans.variant_abs (raw_xn, xT, ta);  (* FIXME !? *)
+            val (xn, ta) = Term.dest_abs (raw_xn, xT, ta);
             val x = Free (xn, xT);
             val cx = Thm.cterm_of ctxt' x;
             val cta = Thm.cterm_of ctxt' ta;
diff -r 71dfb835025d -r 4cdc5e946c99 src/Tools/misc_legacy.ML
--- a/src/Tools/misc_legacy.ML	Sat Oct 02 11:56:11 2021 +0200
+++ b/src/Tools/misc_legacy.ML	Sat Oct 02 12:04:14 2021 +0200
@@ -127,7 +127,7 @@
 fun strip_context_aux (params, Hs, \<^Const_>\<open>Pure.imp for H B\<close>) =
       strip_context_aux (params, H :: Hs, B)
   | strip_context_aux (params, Hs, \<^Const_>\<open>Pure.all _ for \<open>Abs (a, T, t)\<close>\<close>) =
-      let val (b, u) = Syntax_Trans.variant_abs (a, T, t)
+      let val (b, u) = Term.dest_abs (a, T, t)
       in strip_context_aux ((b, T) :: params, Hs, u) end
   | strip_context_aux (params, Hs, B) = (rev params, rev Hs, B);