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/Pure/raw_simplifier.ML
changeset 74518 de4f151c2a34
parent 74509 f24ade4ff3cc
child 74525 c960bfcb91db 
--- a/src/Pure/raw_simplifier.ML	Thu Oct 14 15:24:28 2021 +0200
+++ b/src/Pure/raw_simplifier.ML	Thu Oct 14 16:03:20 2021 +0200
@@ -1134,7 +1134,7 @@
                 let
                     val (v, ctxt') = Variable.next_bound (a, T) ctxt;
                     val b = #1 (Term.dest_Free v);
-                    val (v', t') = Thm.dest_abs (SOME b) t0;
+                    val (v', t') = Thm.dest_abs_name b t0;
                     val b' = #1 (Term.dest_Free (Thm.term_of v'));
                     val _ =
                       if b <> b' then
isabelle