1.1 --- a/src/HOL/Library/RBT.thy	Fri May 21 15:22:37 2010 +0200
     1.2 +++ b/src/HOL/Library/RBT.thy	Fri May 21 15:22:37 2010 +0200
     1.3 @@ -222,7 +222,8 @@
     1.4    "Mapping.bulkload vs = Mapping (bulkload (List.map (\<lambda>n. (n, vs ! n)) [0..<length vs]))"
     1.5    by (rule mapping_eqI) (simp add: map_of_map_restrict expand_fun_eq)
     1.6  
     1.7 -lemma [code, code del]: "HOL.eq (x :: (_, _) mapping) y \<longleftrightarrow> x = y" by (fact eq_equals) (*FIXME*)
     1.8 +lemma [code, code del]:
     1.9 +  "HOL.eq (x :: (_, _) mapping) y \<longleftrightarrow> x = y" by (fact eq_equals) (*FIXME*)
    1.10  
    1.11  lemma eq_Mapping [code]:
    1.12    "HOL.eq (Mapping t1) (Mapping t2) \<longleftrightarrow> entries t1 = entries t2"