more

jvanbruegge · Sep 20, 2024 · c5648d8 · c5648d8
1 parent 00ea9cf
commit c5648d8
Showing 1 changed file with 1 addition and 1 deletion.
diff --git a/thys/Untyped_Lambda_Calculus/LC_pair.thy b/thys/Untyped_Lambda_Calculus/LC_pair.thy
@@ -13,7 +13,7 @@ declare [[mrbnf_internals]]
 binder_datatype 'a "term" =
   Var 'a
 | App "'a term" "'a term"
-| Lam xy ::"'a \<times> 'a" t::"'a term" binds xy in t
+| Lam "x::'a \<times> y::'a" t::"'a term" binds x y in t
 for
   vvsubst: vvsubst
   tvsubst: tvsubst