src/ZF/ind_syntax.ML
changeset 23156 6ec9e29143e9
parent 22567 1565d476a9e2
child 23419 8c30dd4b3b22
     1.1 --- a/src/ZF/ind_syntax.ML	Thu May 31 14:34:06 2007 +0200
     1.2 +++ b/src/ZF/ind_syntax.ML	Thu May 31 14:34:07 2007 +0200
     1.3 @@ -125,7 +125,7 @@
     1.4      let val rec_hds = map head_of rec_tms
     1.5          val dummy = assert_all is_Const rec_hds
     1.6            (fn t => "Datatype set not previously declared as constant: " ^
     1.7 -                   Sign.string_of_term IFOL.thy t);
     1.8 +                   Sign.string_of_term @{theory IFOL} t);
     1.9          val rec_names = (*nat doesn't have to be added*)
    1.10  	    "Nat.nat" :: map (#1 o dest_Const) rec_hds
    1.11  	val u = if co then quniv else univ