--- a/LFex.thy	Fri Nov 27 09:16:32 2009 +0100
+++ b/LFex.thy	Fri Nov 27 10:04:49 2009 +0100
@@ -318,7 +318,7 @@
 apply (tactic {* clean_tac @{context}  defs aps 1 *})
 ML_prf {*  *}
 print_quotients
-apply(tactic {* r_mk_comb_tac' @{context} rty [quot] rel_refl trans2 [] 1*})
+apply(tactic {* r_mk_comb_tac' @{context} rty [quot] rel_refl [trans2] [] 1*})
 
 
 ML {* val consts = lookup_quot_consts defs *}