Mercurial Mercurial > repos > isabelle / diff
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/HOL/Tools/reification.ML
changeset 74525 c960bfcb91db
parent 74408 4cdc5e946c99 
--- a/src/HOL/Tools/reification.ML	Fri Oct 15 17:45:47 2021 +0200
+++ b/src/HOL/Tools/reification.ML	Fri Oct 15 19:25:31 2021 +0200
@@ -136,13 +136,10 @@
     val thy = Proof_Context.theory_of ctxt;
     fun tryabsdecomp (ct, ctxt) bds =
       (case Thm.term_of ct of
-        Abs (_, xT, ta) =>
+        Abs (_, xT, _) =>
           let
-            val ([raw_xn], ctxt') = Variable.variant_fixes ["x"] ctxt;
-            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;
+            val ((cx, cta), ctxt') = Variable.dest_abs_cterm ct ctxt;
+            val x = Thm.term_of cx;
             val bds = (case AList.lookup Type.could_unify bds (HOLogic.listT xT) of
                 NONE => error "tryabsdecomp: Type not found in the Environement"
               | SOME (bsT, atsT) => AList.update Type.could_unify (HOLogic.listT xT,
isabelle