| changeset 74525 | c960bfcb91db |
| parent 74518 | de4f151c2a34 |
| child 74532 | 64d1b02327a4 |
--- a/src/HOL/Library/old_recdef.ML Fri Oct 15 17:45:47 2021 +0200 +++ b/src/HOL/Library/old_recdef.ML Fri Oct 15 19:25:31 2021 +0200 @@ -774,7 +774,7 @@ fun dest_comb t = Thm.dest_comb t handle CTERM (msg, _) => raise ERR "dest_comb" msg; -fun dest_abs t = Thm.dest_abs t +fun dest_abs t = Thm.dest_abs_global t handle CTERM (msg, _) => raise ERR "dest_abs" msg; fun capply t u = Thm.apply t u