diff -r 2b26acbd130c -r c477d0f79ab9 test/Tools/isac/Knowledge/algein.sml
--- a/test/Tools/isac/Knowledge/algein.sml	Mon Dec 07 11:32:12 2015 +0100
+++ b/test/Tools/isac/Knowledge/algein.sml	Mon Dec 07 14:10:59 2015 +0100
@@ -29,7 +29,7 @@
 \ (let t_t = (l_l = 1)\
 \ in t_t)"
 ;
-val sc = ((inst_abs thy) o term_of o the o (parse thy)) str;
+val sc = ((inst_abs thy) o Thm.term_of o the o (parse thy)) str;
 atomty sc;
 atomt sc;