Quot/Examples/FSet.thy
changeset 758 3104d62e7a16
parent 705 f51c6069cd17
child 766 df053507edba
--- a/Quot/Examples/FSet.thy	Wed Dec 16 14:28:48 2009 +0100
+++ b/Quot/Examples/FSet.thy	Thu Dec 17 14:58:33 2009 +0100
@@ -359,7 +359,7 @@
 apply(regularize)
 apply(rule fun_rel_id_asm)
 apply(subst babs_simp)
-apply(tactic {* quotient_tac @{context} 1 *})
+apply(tactic {* Quotient_Tacs.quotient_tac @{context} 1 *})
 apply(rule fun_rel_id_asm)
 apply(rule impI)
 apply(rule mp[OF eq_imp_rel[OF fset_equivp]])