src/HOL/Tools/hologic.ML
changeset 37387 3581483cca6c
parent 37145 01aa36932739
child 37389 09467cdfa198
     1.1 --- a/src/HOL/Tools/hologic.ML	Tue Jun 08 07:45:39 2010 +0200
     1.2 +++ b/src/HOL/Tools/hologic.ML	Tue Jun 08 16:37:19 2010 +0200
     1.3 @@ -438,16 +438,16 @@
     1.4  
     1.5  (* nat *)
     1.6  
     1.7 -val natT = Type ("nat", []);
     1.8 +val natT = Type ("Nat.nat", []);
     1.9  
    1.10  val zero = Const ("Groups.zero_class.zero", natT);
    1.11  
    1.12  fun is_zero (Const ("Groups.zero_class.zero", _)) = true
    1.13    | is_zero _ = false;
    1.14  
    1.15 -fun mk_Suc t = Const ("Suc", natT --> natT) $ t;
    1.16 +fun mk_Suc t = Const ("Nat.Suc", natT --> natT) $ t;
    1.17  
    1.18 -fun dest_Suc (Const ("Suc", _) $ t) = t
    1.19 +fun dest_Suc (Const ("Nat.Suc", _) $ t) = t
    1.20    | dest_Suc t = raise TERM ("dest_Suc", [t]);
    1.21  
    1.22  val Suc_zero = mk_Suc zero;
    1.23 @@ -459,7 +459,7 @@
    1.24    in if n < 0 then raise TERM ("mk_nat: negative number", []) else mk n end;
    1.25  
    1.26  fun dest_nat (Const ("Groups.zero_class.zero", _)) = 0
    1.27 -  | dest_nat (Const ("Suc", _) $ t) = dest_nat t + 1
    1.28 +  | dest_nat (Const ("Nat.Suc", _) $ t) = dest_nat t + 1
    1.29    | dest_nat t = raise TERM ("dest_nat", [t]);
    1.30  
    1.31  val class_size = "Nat.size";