src/HOL/Tools/hologic.ML
changeset 34974 18b41bba42b5
parent 34962 807f6ce0273d
child 35267 8dfd816713c6
     1.1 --- a/src/HOL/Tools/hologic.ML	Thu Jan 28 11:48:43 2010 +0100
     1.2 +++ b/src/HOL/Tools/hologic.ML	Thu Jan 28 11:48:49 2010 +0100
     1.3 @@ -440,9 +440,9 @@
     1.4  
     1.5  val natT = Type ("nat", []);
     1.6  
     1.7 -val zero = Const ("HOL.zero_class.zero", natT);
     1.8 +val zero = Const ("Algebras.zero_class.zero", natT);
     1.9  
    1.10 -fun is_zero (Const ("HOL.zero_class.zero", _)) = true
    1.11 +fun is_zero (Const ("Algebras.zero_class.zero", _)) = true
    1.12    | is_zero _ = false;
    1.13  
    1.14  fun mk_Suc t = Const ("Suc", natT --> natT) $ t;
    1.15 @@ -458,7 +458,7 @@
    1.16        | mk n = mk_Suc (mk (n - 1));
    1.17    in if n < 0 then raise TERM ("mk_nat: negative number", []) else mk n end;
    1.18  
    1.19 -fun dest_nat (Const ("HOL.zero_class.zero", _)) = 0
    1.20 +fun dest_nat (Const ("Algebras.zero_class.zero", _)) = 0
    1.21    | dest_nat (Const ("Suc", _) $ t) = dest_nat t + 1
    1.22    | dest_nat t = raise TERM ("dest_nat", [t]);
    1.23  
    1.24 @@ -508,12 +508,12 @@
    1.25    | add_numerals (Abs (_, _, t)) = add_numerals t
    1.26    | add_numerals _ = I;
    1.27  
    1.28 -fun mk_number T 0 = Const ("HOL.zero_class.zero", T)
    1.29 -  | mk_number T 1 = Const ("HOL.one_class.one", T)
    1.30 +fun mk_number T 0 = Const ("Algebras.zero_class.zero", T)
    1.31 +  | mk_number T 1 = Const ("Algebras.one_class.one", T)
    1.32    | mk_number T i = number_of_const T $ mk_numeral i;
    1.33  
    1.34 -fun dest_number (Const ("HOL.zero_class.zero", T)) = (T, 0)
    1.35 -  | dest_number (Const ("HOL.one_class.one", T)) = (T, 1)
    1.36 +fun dest_number (Const ("Algebras.zero_class.zero", T)) = (T, 0)
    1.37 +  | dest_number (Const ("Algebras.one_class.one", T)) = (T, 1)
    1.38    | dest_number (Const ("Int.number_class.number_of", Type ("fun", [_, T])) $ t) =
    1.39        (T, dest_numeral t)
    1.40    | dest_number t = raise TERM ("dest_number", [t]);