# HG changeset patch
# User nipkow
# Date 1448031102 -3600
# Node ID 62ca03f46ba54fe3e477e89486f4389b2c9a0734
# Parent  e77cb3792503a0afd62f887b185c50ab77264af4
tuned

diff -r e77cb3792503 -r 62ca03f46ba5 src/HOL/Data_Structures/Splay_Set.thy
--- a/src/HOL/Data_Structures/Splay_Set.thy	Fri Nov 20 12:22:50 2015 +0100
+++ b/src/HOL/Data_Structures/Splay_Set.thy	Fri Nov 20 15:51:42 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)"