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




