src/HOL/Nominal/nominal_fresh_fun.ML
changeset 24271 499608101177
parent 23368 ad690b9bca1c
child 24558 419f7cde7f59
     1.1 --- a/src/HOL/Nominal/nominal_fresh_fun.ML	Tue Aug 14 23:22:49 2007 +0200
     1.2 +++ b/src/HOL/Nominal/nominal_fresh_fun.ML	Tue Aug 14 23:22:51 2007 +0200
     1.3 @@ -78,8 +78,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 = Type.of_sort (Sign.tsig_of thy)
     1.8 -     (T, Sign.intern_sort thy ["fs_"^atom_basename]); 
     1.9 +   fun is_of_fs_name T = Sign.of_sort thy (T, Sign.intern_sort thy ["fs_"^atom_basename]); 
    1.10  (* rebuild de bruijn indices *)
    1.11     val bvs = map_index (Bound o fst) ps;
    1.12  (* select variables of the right class *)