1.1 --- a/src/HOL/Nominal/nominal_fresh_fun.ML	Tue Mar 09 14:18:06 2010 +0100
     1.2 +++ b/src/HOL/Nominal/nominal_fresh_fun.ML	Tue Mar 09 14:55:25 2010 +0100
     1.3 @@ -58,7 +58,7 @@
     1.4     val goal = List.nth(prems_of thm, i-1);
     1.5     val ps = Logic.strip_params goal;
     1.6     val Ts = rev (map snd ps);
     1.7 -   fun is_of_fs_name T = Sign.of_sort thy (T, Sign.intern_sort thy ["fs_"^atom_basename]);
     1.8 +   fun is_of_fs_name T = Sign.of_sort thy (T, [Sign.intern_class thy ("fs_"^atom_basename)]);
     1.9  (* rebuild de bruijn indices *)
    1.10     val bvs = map_index (Bound o fst) ps;
    1.11  (* select variables of the right class *)