diff -r 627d25067f2f -r f6374c995ac5 src/Tools/isac/Knowledge/EqSystem.thy
--- a/src/Tools/isac/Knowledge/EqSystem.thy	Fri Mar 02 14:19:59 2018 +0100
+++ b/src/Tools/isac/Knowledge/EqSystem.thy	Fri Mar 02 16:19:02 2018 +0100
@@ -78,9 +78,9 @@
 				       $ vs $ all $ t)) _ =
     if occur_exactly_in (TermC.isalist2list vs) (TermC.isalist2list all) t
     then SOME ((term2str p) ^ " = True",
-	       TermC.Trueprop $ (TermC.mk_equality (p, @{term True})))
+	       HOLogic.Trueprop $ (TermC.mk_equality (p, @{term True})))
     else SOME ((term2str p) ^ " = False",
-	       TermC.Trueprop $ (TermC.mk_equality (p, @{term False})))
+	       HOLogic.Trueprop $ (TermC.mk_equality (p, @{term False})))
   | eval_occur_exactly_in _ _ _ _ = NONE;
 *}
 setup {* KEStore_Elems.add_calcs
@@ -118,7 +118,7 @@
 fun size_of_term' (Free (ccc, _)) =
     (case Symbol.explode ccc of (*WN0510 hack for the bound variables*)
 	"c"::[] => 1000
-      | "c"::"_"::is => 1000 * ((TermC.str2int o implode) is)
+      | "c"::"_"::is => 1000 * ((TermC.int_of_str o implode) is)
       | _ => 1)
   | size_of_term' (Abs (_,_,body)) = 1 + size_of_term' body
   | size_of_term' (f$t) = size_of_term' f  +  size_of_term' t