1.1 --- a/src/Tools/isac/Knowledge/Integrate.thy	Fri Mar 02 14:19:59 2018 +0100
     1.2 +++ b/src/Tools/isac/Knowledge/Integrate.thy	Fri Mar 02 16:19:02 2018 +0100
     1.3 @@ -58,12 +58,12 @@
     1.4      let fun selc var = 
     1.5  	    case (Symbol.explode o id_of) var of
     1.6  		"c"::[] => true
     1.7 -	      |	"c"::"_"::is => (case (TermC.int_of_str o implode) is of
     1.8 +	      |	"c"::"_"::is => (case (TermC.int_of_str_opt o implode) is of
     1.9  				     SOME _ => true
    1.10  				   | NONE => false)
    1.11                | _ => false;
    1.12  	fun get_coeff c = case (Symbol.explode o id_of) c of
    1.13 -	      		      "c"::"_"::is => (the o TermC.int_of_str o implode) is
    1.14 +	      		      "c"::"_"::is => (the o TermC.int_of_str_opt o implode) is
    1.15  			    | _ => 0;
    1.16          val cs = filter selc (TermC.vars term);
    1.17      in 
    1.18 @@ -93,7 +93,7 @@
    1.19  		     Const ("HOL.eq", T) $ lh $ TermC.mk_add rh (new_c rh)
    1.20  		   | p => TermC.mk_add p (new_c p)
    1.21      in SOME ((term2str p) ^ " = " ^ term2str p',
    1.22 -	  TermC.Trueprop $ (TermC.mk_equality (p, p')))
    1.23 +	  HOLogic.Trueprop $ (TermC.mk_equality (p, p')))
    1.24      end
    1.25    | eval_add_new_c _ _ _ _ = NONE;
    1.26  
    1.27 @@ -103,9 +103,9 @@
    1.28  					   $ arg)) _ =
    1.29      if TermC.is_f_x arg
    1.30      then SOME ((term2str p) ^ " = True",
    1.31 -	       TermC.Trueprop $ (TermC.mk_equality (p, @{term True})))
    1.32 +	       HOLogic.Trueprop $ (TermC.mk_equality (p, @{term True})))
    1.33      else SOME ((term2str p) ^ " = False",
    1.34 -	       TermC.Trueprop $ (TermC.mk_equality (p, @{term False})))
    1.35 +	       HOLogic.Trueprop $ (TermC.mk_equality (p, @{term False})))
    1.36    | eval_is_f_x _ _ _ _ = NONE;
    1.37  *}
    1.38  setup {* KEStore_Elems.add_calcs