     1.1 --- a/src/HOL/ex/ROOT.ML	Wed May 30 10:04:05 2012 +0200
     1.2 +++ b/src/HOL/ex/ROOT.ML	Wed May 30 16:05:06 2012 +0200
     1.3 @@ -12,7 +12,7 @@
     1.4    "Hebrew",
     1.5    "Chinese",
     1.6    "Serbian",
     1.7 -  "~~/src/HOL/Library/FinFun"
     1.8 +  "~~/src/HOL/Library/FinFun_Syntax"
     1.9  ];
    1.10  
    1.11  use_thys [
changeset 49056	d60f6b41bf2d
parent 49043	a5377f6d9f14
child 49064	d862b0d56c49