# HG changeset patch
# User nipkow
# Date 1448031110 -3600
# Node ID e346691e7f20ce1362d1f2d495514821f7c82801
# Parent  21d7910d681603dc2458ec0b5b63d285f23bb8f3# Parent  62ca03f46ba54fe3e477e89486f4389b2c9a0734
merged

diff -r 21d7910d6816 -r e346691e7f20 src/HOL/Data_Structures/Splay_Set.thy
--- a/src/HOL/Data_Structures/Splay_Set.thy	Fri Nov 20 14:44:53 2015 +0000
+++ b/src/HOL/Data_Structures/Splay_Set.thy	Fri Nov 20 15:51:50 2015 +0100
@@ -77,7 +77,7 @@
 by(auto cong: case_tree_cong split: tree.split)
 
 definition is_root :: "'a \<Rightarrow> 'a tree \<Rightarrow> bool" where
-"is_root a t = (case t of Leaf \<Rightarrow> False | Node _ x _ \<Rightarrow> x = a)"
+"is_root x t = (case t of Leaf \<Rightarrow> False | Node l a r \<Rightarrow> x = a)"
 
 definition "isin t x = is_root x (splay x t)"