1.1 --- a/src/Tools/isac/ProgLang/Prog_Expr.thy	Sun Aug 22 11:42:55 2021 +0200
     1.2 +++ b/src/Tools/isac/ProgLang/Prog_Expr.thy	Sun Aug 22 14:28:38 2021 +0200
     1.3 @@ -48,19 +48,15 @@
     1.4  ML \<open>
     1.5  signature PROG_EXPR =
     1.6    sig
     1.7 -(*//------------------------- from Tools .thy-------------------------------------------------\\*)
     1.8 -    val lhs: term -> term
     1.9      val eval_lhs: 'a -> string -> term -> 'b -> (string * term) option
    1.10      val eval_matches: string -> string -> term -> theory -> (string * term) option
    1.11      val matchsub: theory -> term -> term -> bool
    1.12      val eval_matchsub: string -> string -> term -> theory -> (string * term) option
    1.13 -    val rhs: term -> term
    1.14      val eval_rhs: 'a -> string -> term -> 'b -> (string * term) option
    1.15      val eval_var: string -> string -> term -> theory -> (string * term) option
    1.16  
    1.17      val or2list: term -> term
    1.18 -(*\\------------------------- from Tools .thy-------------------------------------------------//*)
    1.19 -(*//------------------------- from Atools .thy------------------------------------------------\\*)
    1.20 +
    1.21      val occurs_in: term -> term -> bool
    1.22      val eval_occurs_in: 'a -> string -> term -> 'b -> (string * term) option
    1.23      val some_occur_in: term list -> term -> bool
    1.24 @@ -221,9 +217,6 @@
    1.25      in SOME (thmId, HOLogic.Trueprop $ (TermC.mk_equality (t, t'))) end
    1.26    | eval_var _ _ _ _ = NONE;
    1.27  
    1.28 -(* refer to Thm.lhs_of *)
    1.29 -fun lhs (Const (\<^const_name>\<open>HOL.eq\<close>,_) $ l $ _) = l
    1.30 -  | lhs t = raise ERROR("lhs called with (" ^ UnparseC.term t ^ ")");
    1.31  (*("lhs"    ,("Prog_Expr.lhs"    , eval_lhs "")):calc*)
    1.32  fun eval_lhs _ "Prog_Expr.lhs" (t as (Const (\<^const_name>\<open>lhs\<close>,_) $ (Const (\<^const_name>\<open>HOL.eq\<close>,_) $ l $ _))) _ = 
    1.33      SOME ((UnparseC.term t) ^ " = " ^ (UnparseC.term l),
    1.34 @@ -502,7 +495,7 @@
    1.35  		  (p as Const ("Prog_Expr.boollist2sum", _) $ (l as Const (\<^const_name>\<open>Cons\<close>, _) $ _ $ _)) _ =
    1.36      let
    1.37        val isal = TermC.isalist2list l
    1.38 -	    val lhss = map lhs isal
    1.39 +	    val lhss = map TermC.lhs isal
    1.40  	    val sum = list2sum lhss
    1.41      in
    1.42        SOME ((UnparseC.term p) ^ " = " ^ (UnparseC.term sum),