--- a/src/HOL/ex/ROOT.ML Wed May 30 10:04:05 2012 +0200 +++ b/src/HOL/ex/ROOT.ML Wed May 30 16:05:06 2012 +0200 @@ -12,7 +12,7 @@ "Hebrew", "Chinese", "Serbian", - "~~/src/HOL/Library/FinFun" + "~~/src/HOL/Library/FinFun_Syntax" ]; use_thys [