src/HOL/Nominal/Nominal.thy

 primrec (unchecked perm_nprod)
   perm_nProd_def: "pi\<bullet>(nPair x1 x2)  = nPair (pi\<bullet>x1) (pi\<bullet>x2)"
 
 (* permutation on characters (used in strings) *)
 defs (unchecked overloaded)
-  perm_char_def: "pi\<bullet>(s::char) \<equiv> s"
+  perm_char_def: "pi\<bullet>(c::char) \<equiv> c"
+
+lemma perm_string:
+  fixes s::"string"
+  shows "pi\<bullet>s = s"
+by (induct s)(auto simp add: perm_char_def)
 
 (* permutation on ints *)
 defs (unchecked overloaded)
   perm_int_def:    "pi\<bullet>(i::int) \<equiv> i"
 

   done
   
 lemma supp_string:
   fixes s::"string"
   shows "supp (s) = {}"
-apply(induct s)
-apply(auto simp add: supp_char supp_list_nil supp_list_cons)
+apply(simp add: supp_def perm_string)
 done
 
 lemma fresh_set_empty:
   shows "a\<sharp>{}"
   by (simp add: fresh_def supp_set_empty)