# HG changeset patch
# User wenzelm
# Date 1630350613 -7200
# Node ID e16ac8907148a66d5188c9d8909a007702537029
# Parent  12152390db34738708c266154a47269b1e86cea9
tuned signature;

diff -r 12152390db34 -r e16ac8907148 src/Tools/Haskell/Haskell.thy
--- a/src/Tools/Haskell/Haskell.thy	Sun Aug 29 13:16:22 2021 +0200
+++ b/src/Tools/Haskell/Haskell.thy	Mon Aug 30 21:10:13 2021 +0200
@@ -2257,7 +2257,7 @@
 
 module Isabelle.Term (
   Indexname, Sort, Typ(..), Term(..),
-  Free, lambda, declare_frees, incr_boundvars, subst_bound, dest_abs, strip_abs,
+  Free, lambda, declare_frees, incr_boundvars, subst_bound, dest_lambda, strip_lambda,
   type_op0, type_op1, op0, op1, op2, typed_op0, typed_op1, typed_op2, binder,
   dummyS, dummyT, is_dummyT, propT, is_propT, (-->), dest_funT, (--->),
   aconv, list_comb, strip_comb, head_of
@@ -2331,19 +2331,19 @@
     subst lev (App (t, u)) = App (subst lev t, subst lev u)
     subst _ t = t
 
-dest_abs :: Name.Context -> Term -> Maybe (Free, Term)
-dest_abs names (Abs (x, ty, b)) =
+dest_lambda :: Name.Context -> Term -> Maybe (Free, Term)
+dest_lambda names (Abs (x, ty, b)) =
   let
     (x', _) = Name.variant x (declare_frees b names)
     v = (x', ty)
   in Just (v, subst_bound (Free v) b)
-dest_abs _ _ = Nothing
-
-strip_abs :: Name.Context -> Term -> ([Free], Term)
-strip_abs names tm =
-  case dest_abs names tm of
+dest_lambda _ _ = Nothing
+
+strip_lambda :: Name.Context -> Term -> ([Free], Term)
+strip_lambda names tm =
+  case dest_lambda names tm of
     Just (v, t) ->
-      let (vs, t') = strip_abs names t'
+      let (vs, t') = strip_lambda names t'
       in (v : vs, t')
     Nothing -> ([], tm)
 
@@ -2417,7 +2417,7 @@
 binder name = (mk, dest)
   where
     mk (a, ty) b = App (Const (name, [ty]), lambda (a, ty) b)
-    dest names (App (Const (c, _), t)) | c == name = dest_abs names t
+    dest names (App (Const (c, _), t)) | c == name = dest_lambda names t
     dest _ _ = Nothing