diff -r 40e3e6a6076f -r bb7f4457091a Quot/Nominal/Test.thy --- a/Quot/Nominal/Test.thy Mon Feb 08 11:56:22 2010 +0100 +++ b/Quot/Nominal/Test.thy Mon Feb 08 13:12:55 2010 +0100 @@ -110,12 +110,12 @@ [] => set | B (s1, s2) :: tl => if s2 = s then - fv_bds s tl (HOLogic.mk_binop @{const_name "HOL.minus_class.minus"} (set, HOLogic.mk_set @{typ name} [Free (s1, @{typ name})])) + fv_bds s tl (HOLogic.mk_binop @{const_name "Algebras.minus_class.minus"} (set, HOLogic.mk_set @{typ name} [Free (s1, @{typ name})])) else fv_bds s tl set | BS (s1, s2) :: tl => (* TODO: This is just a copy *) if s2 = s then - fv_bds s tl (HOLogic.mk_binop @{const_name "HOL.minus_class.minus"} (set, HOLogic.mk_set @{typ name} [Free (s1, @{typ name})])) + fv_bds s tl (HOLogic.mk_binop @{const_name "Algebras.minus_class.minus"} (set, HOLogic.mk_set @{typ name} [Free (s1, @{typ name})])) else fv_bds s tl set *}