Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
tuned -- eliminated Sign.intern_sort;
authorwenzelm
Tue, 09 Mar 2010 14:55:25 +0100
changeset 35667 aa59452c913c
parent 35666 6fd0ca1a3966
child 35668 69e1740fbfb1
tuned -- eliminated Sign.intern_sort;
src/HOL/Nominal/nominal_fresh_fun.ML file | annotate | diff | comparison | revisions 
--- 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 *)
isabelle