--- 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
*}