changeset 59188 | c477d0f79ab9 |
parent 55446 | 42c45d1241d7 |
child 59248 | 5eba5e6d5266 |
1.1 --- a/test/Tools/isac/Knowledge/algein.sml Mon Dec 07 11:32:12 2015 +0100 1.2 +++ b/test/Tools/isac/Knowledge/algein.sml Mon Dec 07 14:10:59 2015 +0100 1.3 @@ -29,7 +29,7 @@ 1.4 \ (let t_t = (l_l = 1)\ 1.5 \ in t_t)" 1.6 ; 1.7 -val sc = ((inst_abs thy) o term_of o the o (parse thy)) str; 1.8 +val sc = ((inst_abs thy) o Thm.term_of o the o (parse thy)) str; 1.9 atomty sc; 1.10 atomt sc; 1.11