--- a/LFex.thy	Sat Dec 05 21:50:31 2009 +0100
+++ b/LFex.thy	Sat Dec 05 22:02:32 2009 +0100
@@ -270,6 +270,8 @@
 ML_prf {* PolyML.profiling 1 *}
 ML_prf {* profile 2 Seq.list_of ((all_inj_repabs_tac @{context} quot rel_refl trans2 1) (#goal (Isar.goal ()))) *}
 *)
+apply(unfold perm_kind_def perm_ty_def perm_trm_def)
+apply(tactic {* clean_tac @{context} 1 *})
 done
 
 (* Does not work: