src/HOL/OrderedGroup.thy
changeset 24137 8d7896398147
parent 23879 4776af8be741
child 24286 7619080e49f0
     1.1 --- a/src/HOL/OrderedGroup.thy	Thu Aug 02 23:18:13 2007 +0200
     1.2 +++ b/src/HOL/OrderedGroup.thy	Fri Aug 03 16:28:15 2007 +0200
     1.3 @@ -1104,7 +1104,7 @@
     1.4    
     1.5  val eq_reflection = @{thm eq_reflection};
     1.6    
     1.7 -val thy_ref = Theory.self_ref @{theory};
     1.8 +val thy_ref = Theory.check_thy @{theory};
     1.9  
    1.10  val T = TFree("'a", ["OrderedGroup.ab_group_add"]);
    1.11