# HG changeset patch
# User wenzelm
# Date 1633367544 -7200
# Node ID 5f9c51c2fc0a95e6ea7a22e2119f183d0c6174e8
# Parent  2fdf37577f7b1fce6dd3fe0771e2cb98133a28c8
proper term operation Term.dest_abs;

diff -r 2fdf37577f7b -r 5f9c51c2fc0a src/Tools/Code/code_thingol.ML
--- a/src/Tools/Code/code_thingol.ML	Mon Oct 04 18:19:16 2021 +0200
+++ b/src/Tools/Code/code_thingol.ML	Mon Oct 04 19:12:24 2021 +0200
@@ -622,7 +622,7 @@
       pair (IVar (SOME v))
   | translate_term ctxt algbr eqngr permissive some_thm (Abs (v, ty, t), some_abs) =
       let
-        val (v', t') = Syntax_Trans.variant_abs (Name.desymbolize (SOME false) v, ty, t);
+        val (v', t') = Term.dest_abs (Name.desymbolize (SOME false) v, ty, t);
         val v'' = if Term.used_free v' t' then SOME v' else NONE
       in
         translate_typ ctxt algbr eqngr permissive ty