1.1 --- a/src/Tools/isac/ProgLang/Prog_Expr.thy	Tue Jul 13 09:49:45 2021 +0200
     1.2 +++ b/src/Tools/isac/ProgLang/Prog_Expr.thy	Tue Jul 13 10:43:21 2021 +0200
     1.3 @@ -281,9 +281,9 @@
     1.4  (*("is_atom",("Prog_Expr.is_atom", Prog_Expr.eval_is_atom "#is_atom_"))*)
     1.5  fun eval_is_atom (thmid:string) "Prog_Expr.is_atom" (t as (Const _ $ arg)) _ = 
     1.6      if TermC.is_atom arg
     1.7 -    then SOME (TermC.mk_thmid thmid "" "", 
     1.8 +    then SOME (TermC.mk_thmid thmid (TermC.string_of_atom arg) "", 
     1.9  			HOLogic.Trueprop $ (TermC.mk_equality (t, @{term True})))
    1.10 -    else SOME (TermC.mk_thmid thmid "" "", 
    1.11 +    else SOME (TermC.mk_thmid thmid (TermC.string_of_atom arg) "", 
    1.12  		  HOLogic.Trueprop $ (TermC.mk_equality (t, @{term False})))
    1.13    | eval_is_atom _ _ _ _ = NONE;
    1.14