1.1 --- a/src/Tools/isac/ProgLang/Prog_Expr.thy	Mon Jul 12 17:21:37 2021 +0200
     1.2 +++ b/src/Tools/isac/ProgLang/Prog_Expr.thy	Tue Jul 13 08:52:35 2021 +0200
     1.3 @@ -279,13 +279,12 @@
     1.4    | eval_some_occur_in _ _ _ _ = NONE;
     1.5  
     1.6  (*("is_atom",("Prog_Expr.is_atom", Prog_Expr.eval_is_atom "#is_atom_"))*)
     1.7 -fun eval_is_atom (thmid:string) "Prog_Expr.is_atom"
     1.8 -		 (t as (Const _ $ arg)) _ = 
     1.9 -    (case arg of 
    1.10 -	 Free (n,_) => SOME (TermC.mk_thmid thmid n "", 
    1.11 -			      HOLogic.Trueprop $ (TermC.mk_equality (t, @{term True})))
    1.12 -       | _ => SOME (TermC.mk_thmid thmid "" "", 
    1.13 -		    HOLogic.Trueprop $ (TermC.mk_equality (t, @{term False}))))
    1.14 +fun eval_is_atom (thmid:string) "Prog_Expr.is_atom" (t as (Const _ $ arg)) _ = 
    1.15 +    if TermC.is_atom arg
    1.16 +    then SOME (TermC.mk_thmid thmid "" "", 
    1.17 +			HOLogic.Trueprop $ (TermC.mk_equality (t, @{term True})))
    1.18 +    else SOME (TermC.mk_thmid thmid "" "", 
    1.19 +		  HOLogic.Trueprop $ (TermC.mk_equality (t, @{term False})))
    1.20    | eval_is_atom _ _ _ _ = NONE;
    1.21  
    1.22  fun even i = (i div 2) * 2 = i;