src/HOL/Data_Structures/AA_Set.thy
changeset 62160 ff20b44b2fc8
parent 62130 90a3016a6c12
child 62390 842917225d56
     1.1 --- a/src/HOL/Data_Structures/AA_Set.thy	Wed Jan 13 00:12:43 2016 +0100
     1.2 +++ b/src/HOL/Data_Structures/AA_Set.thy	Wed Jan 13 09:38:16 2016 +0100
     1.3 @@ -72,7 +72,7 @@
     1.4      else
     1.5        case r of
     1.6          Leaf \<Rightarrow> Leaf (* unreachable *) |
     1.7 -        Node _ t1 b t4 \<Rightarrow>
     1.8 +        Node lvb t1 b t4 \<Rightarrow>
     1.9            (case t1 of
    1.10               Node lva t2 a t3
    1.11                 \<Rightarrow> Node (lva+1) (Node (lv-1) l x t2) a