src/HOL/Tools/int_arith.ML
changeset 36945 9bec62c10714
parent 35267 8dfd816713c6
child 38715 6513ea67d95d
     1.1 --- a/src/HOL/Tools/int_arith.ML	Sat May 15 21:41:32 2010 +0200
     1.2 +++ b/src/HOL/Tools/int_arith.ML	Sat May 15 21:50:05 2010 +0200
     1.3 @@ -21,7 +21,7 @@
     1.4     That is, m and n consist only of 1s combined with "+", "-" and "*".
     1.5  *)
     1.6  
     1.7 -val zeroth = (symmetric o mk_meta_eq) @{thm of_int_0};
     1.8 +val zeroth = (Thm.symmetric o mk_meta_eq) @{thm of_int_0};
     1.9  
    1.10  val lhss0 = [@{cpat "0::?'a::ring"}];
    1.11  
    1.12 @@ -35,7 +35,7 @@
    1.13    make_simproc {lhss = lhss0, name = "zero_to_of_int_zero_simproc",
    1.14    proc = proc0, identifier = []};
    1.15  
    1.16 -val oneth = (symmetric o mk_meta_eq) @{thm of_int_1};
    1.17 +val oneth = (Thm.symmetric o mk_meta_eq) @{thm of_int_1};
    1.18  
    1.19  val lhss1 = [@{cpat "1::?'a::ring_1"}];
    1.20