--- a/LFex.thy	Wed Dec 02 23:11:50 2009 +0100
+++ b/LFex.thy	Wed Dec 02 23:31:30 2009 +0100
@@ -267,7 +267,7 @@
 apply(tactic {* regularize_tac @{context} @{thms alpha_EQUIVs} 1 *})
 prefer 2
 apply(tactic {* clean_tac @{context} quot defs 1 *})
-apply(tactic {* all_inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2  1*})
+apply(tactic {* all_inj_repabs_tac @{context} quot rel_refl trans2  1*})
 done
 
 (* Does not work:
@@ -296,7 +296,7 @@
   \<Longrightarrow> P1 mkind \<and> P2 mty \<and> P3 mtrm"
 apply(tactic {* procedure_tac @{context} @{thm kind_ty_trm.induct} 1 *})
 apply(tactic {* regularize_tac @{context} @{thms alpha_EQUIVs} 1 *})
-apply(tactic {* all_inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 1 *})
+apply(tactic {* all_inj_repabs_tac @{context} quot rel_refl trans2 1 *})
 apply(tactic {* clean_tac @{context} quot defs 1 *})
 done