# HG changeset patch
# User wenzelm
# Date 1268142925 -3600
# Node ID aa59452c913c2cb3eda017590298f0177c1a8dcd
# Parent  6fd0ca1a39668cc527b988a01a69f47ba5ad724d
tuned -- eliminated Sign.intern_sort;

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