1.1 --- a/src/HOL/Nominal/nominal_fresh_fun.ML	Sat Apr 16 16:37:21 2011 +0200
     1.2 +++ b/src/HOL/Nominal/nominal_fresh_fun.ML	Sat Apr 16 18:11:20 2011 +0200
     1.3 @@ -55,7 +55,7 @@
     1.4     val thy = theory_of_thm thm;
     1.5  (* the parsing function returns a qualified name, we get back the base name *)
     1.6     val atom_basename = Long_Name.base_name atom_name;
     1.7 -   val goal = List.nth(prems_of thm, i-1);
     1.8 +   val goal = nth (prems_of thm) (i - 1);
     1.9     val ps = Logic.strip_params goal;
    1.10     val Ts = rev (map snd ps);
    1.11     fun is_of_fs_name T = Sign.of_sort thy (T, [Sign.intern_class thy ("fs_"^atom_basename)]);
    1.12 @@ -97,7 +97,7 @@
    1.13  
    1.14  fun generate_fresh_fun_tac i thm =
    1.15    let
    1.16 -    val goal = List.nth(prems_of thm, i-1);
    1.17 +    val goal = nth (prems_of thm) (i - 1);
    1.18      val atom_name_opt = get_inner_fresh_fun goal;
    1.19    in
    1.20    case atom_name_opt of