src/HOL/OrderedGroup.ML
changeset 16423 24abe4c0e4b4
parent 14755 5cc6e6b9e27a
child 16568 e02fe7ae212b
     1.1 --- a/src/HOL/OrderedGroup.ML	Fri Jun 17 18:33:03 2005 +0200
     1.2 +++ b/src/HOL/OrderedGroup.ML	Fri Jun 17 18:33:03 2005 +0200
     1.3 @@ -8,7 +8,7 @@
     1.4    val ss = simpset_of HOL.thy
     1.5    val eq_reflection = thm "eq_reflection"
     1.6    
     1.7 -  val sg_ref = Sign.self_ref (sign_of (theory "OrderedGroup"))
     1.8 +  val thy_ref = Theory.self_ref (theory "OrderedGroup")
     1.9  
    1.10    val T = TFree("'a", ["OrderedGroup.ab_group_add"])
    1.11