src/HOL/Tools/hologic.ML

--- a/src/HOL/Tools/hologic.ML	Thu Jan 28 11:48:43 2010 +0100
+++ b/src/HOL/Tools/hologic.ML	Thu Jan 28 11:48:49 2010 +0100
@@ -440,9 +440,9 @@
 
 val natT = Type ("nat", []);
 
-val zero = Const ("HOL.zero_class.zero", natT);
+val zero = Const ("Algebras.zero_class.zero", natT);
 
-fun is_zero (Const ("HOL.zero_class.zero", _)) = true
+fun is_zero (Const ("Algebras.zero_class.zero", _)) = true
   | is_zero _ = false;
 
 fun mk_Suc t = Const ("Suc", natT --> natT) $ t;
@@ -458,7 +458,7 @@
       | mk n = mk_Suc (mk (n - 1));
   in if n < 0 then raise TERM ("mk_nat: negative number", []) else mk n end;
 
-fun dest_nat (Const ("HOL.zero_class.zero", _)) = 0
+fun dest_nat (Const ("Algebras.zero_class.zero", _)) = 0
   | dest_nat (Const ("Suc", _) $ t) = dest_nat t + 1
   | dest_nat t = raise TERM ("dest_nat", [t]);
 
@@ -508,12 +508,12 @@
   | add_numerals (Abs (_, _, t)) = add_numerals t
   | add_numerals _ = I;
 
-fun mk_number T 0 = Const ("HOL.zero_class.zero", T)
-  | mk_number T 1 = Const ("HOL.one_class.one", T)
+fun mk_number T 0 = Const ("Algebras.zero_class.zero", T)
+  | mk_number T 1 = Const ("Algebras.one_class.one", T)
   | mk_number T i = number_of_const T $ mk_numeral i;
 
-fun dest_number (Const ("HOL.zero_class.zero", T)) = (T, 0)
-  | dest_number (Const ("HOL.one_class.one", T)) = (T, 1)
+fun dest_number (Const ("Algebras.zero_class.zero", T)) = (T, 0)
+  | dest_number (Const ("Algebras.one_class.one", T)) = (T, 1)
   | dest_number (Const ("Int.number_class.number_of", Type ("fun", [_, T])) $ t) =
       (T, dest_numeral t)
   | dest_number t = raise TERM ("dest_number", [t]);