1.1 --- a/src/HOL/Nominal/Nominal.thy	Sun Aug 28 13:13:27 2011 +0200
     1.2 +++ b/src/HOL/Nominal/Nominal.thy	Sun Aug 28 14:16:14 2011 +0200
     1.3 @@ -3608,7 +3608,7 @@
     1.4  
     1.5  (************************************************************)
     1.6  (* various tactics for analysing permutations, supports etc *)
     1.7 -use "nominal_permeq.ML";
     1.8 +use "nominal_permeq.ML"
     1.9  
    1.10  method_setup perm_simp =
    1.11    {* NominalPermeq.perm_simp_meth *}
    1.12 @@ -3652,7 +3652,7 @@
    1.13  
    1.14  (*****************************************************************)
    1.15  (* tactics for generating fresh names and simplifying fresh_funs *)
    1.16 -use "nominal_fresh_fun.ML";
    1.17 +use "nominal_fresh_fun.ML"
    1.18  
    1.19  method_setup generate_fresh = 
    1.20    {* setup_generate_fresh *} 
    1.21 @@ -3681,7 +3681,7 @@
    1.22  
    1.23  (*****************************************)
    1.24  (* setup for induction principles method *)
    1.25 -use "nominal_induct.ML";
    1.26 +use "nominal_induct.ML"
    1.27  method_setup nominal_induct =
    1.28    {* NominalInduct.nominal_induct_method *}
    1.29    {* nominal induction *}