1.1 --- a/src/Tools/isac/ProgLang/Prog_Expr.thy	Wed Oct 02 15:14:51 2019 +0200
     1.2 +++ b/src/Tools/isac/ProgLang/Prog_Expr.thy	Wed Oct 02 16:02:17 2019 +0200
     1.3 @@ -258,8 +258,8 @@
     1.4  (*("occurs_in", ("Prog_Expr.occurs'_in", Prog_Expr.eval_occurs_in ""))*)
     1.5  fun eval_occurs_in _ "Prog_Expr.occurs'_in"
     1.6  	     (p as (Const ("Prog_Expr.occurs'_in",_) $ v $ t)) _ =
     1.7 -    ((*tracing("@@@ eval_occurs_in: v= "^(Rule.term2str v));
     1.8 -     tracing("@@@ eval_occurs_in: t= "^(Rule.term2str t));*)
     1.9 +    ((*tracing("#>@ eval_occurs_in: v= "^(Rule.term2str v));
    1.10 +     tracing("#>@ eval_occurs_in: t= "^(Rule.term2str t));*)
    1.11       if occurs_in v t
    1.12      then SOME ((Rule.term2str p) ^ " = True",
    1.13  	  HOLogic.Trueprop $ (TermC.mk_equality (p, @{term True})))
    1.14 @@ -474,7 +474,7 @@
    1.15      	        val prop = HOLogic.Trueprop $ (TermC.mk_equality (t, rhs))
    1.16      	    in SOME (TermC.mk_thmid thmid n1 n2, prop) end
    1.17          end
    1.18 -      | _ => ((*tracing"@@@ eval_cancel NONE";*)NONE))
    1.19 +      | _ => ((*tracing"#>@ eval_cancel NONE";*)NONE))
    1.20    | eval_cancel _ _ _ _ = NONE;
    1.21  
    1.22  (* get the argument from a function-definition *)