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




