src/HOL/Integ/int_arith1.ML
changeset 16423 24abe4c0e4b4
parent 15965 f422f8283491
child 16473 b24c820a0b85
     1.1 --- a/src/HOL/Integ/int_arith1.ML	Fri Jun 17 18:33:03 2005 +0200
     1.2 +++ b/src/HOL/Integ/int_arith1.ML	Fri Jun 17 18:33:03 2005 +0200
     1.3 @@ -466,7 +466,7 @@
     1.4  struct
     1.5    val ss                = HOL_ss
     1.6    val eq_reflection     = eq_reflection
     1.7 -  val sg_ref = Sign.self_ref (Theory.sign_of (the_context ()))
     1.8 +  val thy_ref = Theory.self_ref (the_context ())
     1.9    val add_ac = mult_ac
    1.10  end;
    1.11