Quot/Nominal/Test.thy
changeset 1087 bb7f4457091a
parent 1034 c1af17982f98
child 1194 3d54fcc5f41a
--- 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
 *}