1.1 --- a/src/Tools/isac/Knowledge/EqSystem.thy	Fri Mar 02 14:19:59 2018 +0100
     1.2 +++ b/src/Tools/isac/Knowledge/EqSystem.thy	Fri Mar 02 16:19:02 2018 +0100
     1.3 @@ -78,9 +78,9 @@
     1.4  				       $ vs $ all $ t)) _ =
     1.5      if occur_exactly_in (TermC.isalist2list vs) (TermC.isalist2list all) t
     1.6      then SOME ((term2str p) ^ " = True",
     1.7 -	       TermC.Trueprop $ (TermC.mk_equality (p, @{term True})))
     1.8 +	       HOLogic.Trueprop $ (TermC.mk_equality (p, @{term True})))
     1.9      else SOME ((term2str p) ^ " = False",
    1.10 -	       TermC.Trueprop $ (TermC.mk_equality (p, @{term False})))
    1.11 +	       HOLogic.Trueprop $ (TermC.mk_equality (p, @{term False})))
    1.12    | eval_occur_exactly_in _ _ _ _ = NONE;
    1.13  *}
    1.14  setup {* KEStore_Elems.add_calcs
    1.15 @@ -118,7 +118,7 @@
    1.16  fun size_of_term' (Free (ccc, _)) =
    1.17      (case Symbol.explode ccc of (*WN0510 hack for the bound variables*)
    1.18  	"c"::[] => 1000
    1.19 -      | "c"::"_"::is => 1000 * ((TermC.str2int o implode) is)
    1.20 +      | "c"::"_"::is => 1000 * ((TermC.int_of_str o implode) is)
    1.21        | _ => 1)
    1.22    | size_of_term' (Abs (_,_,body)) = 1 + size_of_term' body
    1.23    | size_of_term' (f$t) = size_of_term' f  +  size_of_term' t