1.1 --- a/src/Tools/isac/ProgLang/Prog_Expr.thy	Tue May 24 12:57:47 2022 +0200
     1.2 +++ b/src/Tools/isac/ProgLang/Prog_Expr.thy	Tue May 24 16:47:31 2022 +0200
     1.3 @@ -150,13 +150,6 @@
     1.4      SOME ((UnparseC.term t) ^ " = " ^ (UnparseC.term l),
     1.5  	  HOLogic.Trueprop $ (TermC.mk_equality (t, l)))
     1.6    | eval_lhs _ _ _ _ = NONE;
     1.7 -(*
     1.8 -> val t = (Thm.term_of o the o (parse thy)) "lhs (1 * x \<up> 2 = 0)";
     1.9 -> val SOME (id,t') = eval_lhs 0 0 t 0;
    1.10 -val id = "Prog_Expr.lhs (1 * x \<up> 2 = 0) = 1 * x \<up> 2" : string
    1.11 -> term2str t';
    1.12 -val it = "Prog_Expr.lhs (1 * x \<up> 2 = 0) = 1 * x \<up> 2" : string
    1.13 -*)
    1.14  
    1.15  fun rhs (Const (\<^const_name>\<open>HOL.eq\<close>,_) $ _ $ r) = r
    1.16    | rhs t = raise ERROR("rhs called with (" ^ UnparseC.term t ^ ")");