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/Quotient/quotient_tacs.ML
changeset 74525 c960bfcb91db
parent 74282 c2ee8d993d6a
child 77879 dd222e2af01a 
--- a/src/HOL/Tools/Quotient/quotient_tacs.ML	Fri Oct 15 17:45:47 2021 +0200
+++ b/src/HOL/Tools/Quotient/quotient_tacs.ML	Fri Oct 15 19:25:31 2021 +0200
@@ -221,7 +221,7 @@
 
 fun unlam t =
   (case t of
-    Abs a => snd (Term.dest_abs a)
+    Abs _ => snd (Term.dest_abs_global t)
   | _ => unlam (Abs("", domain_type (fastype_of t), (incr_boundvars 1 t) $ (Bound 0))))
 
 val bare_concl = HOLogic.dest_Trueprop o Logic.strip_assums_concl
isabelle