1.1 --- a/src/Tools/isac/ProgLang/Prog_Expr.thy	Sat Sep 14 16:15:05 2019 +0200
     1.2 +++ b/src/Tools/isac/ProgLang/Prog_Expr.thy	Mon Sep 16 12:43:43 2019 +0200
     1.3 @@ -52,9 +52,6 @@
     1.4  signature PROG_EXPR =
     1.5    sig
     1.6  (*//------------------------- from Tools .thy-------------------------------------------------\\*)
     1.7 -    val EmptyList: term
     1.8 -    val UniversalList: term
     1.9 -
    1.10      val lhs: term -> term
    1.11      val eval_lhs: 'a -> string -> term -> 'b -> (string * term) option
    1.12      val eval_matches: string -> string -> term -> theory -> (string * term) option
    1.13 @@ -94,15 +91,10 @@
    1.14  structure Prog_Expr(**): PROG_EXPR =(**)
    1.15  struct
    1.16  (**)
    1.17 -(*//------------------------- from Tools .thy-------------------------------------------------\\*)
    1.18 -(* auxiliary functions for scripts  WN.9.00*)
    1.19 -(*11.02: for equation solving only*)
    1.20 -val UniversalList = (Thm.term_of o the o (TermC.parse @{theory})) "UniversalList";
    1.21 -val EmptyList = (Thm.term_of o the o (TermC.parse @{theory}))  "[]::bool list";     
    1.22  
    1.23  (*+ for Or_to_List +*)
    1.24 -fun or2list (Const ("HOL.True",_)) = (tracing"### or2list True";UniversalList)
    1.25 -  | or2list (Const ("HOL.False",_)) = (tracing"### or2list False";EmptyList)
    1.26 +fun or2list (Const ("HOL.True",_)) = (tracing"### or2list True"; UniversalList)
    1.27 +  | or2list (Const ("HOL.False",_)) = (tracing"### or2list False"; EmptyList)
    1.28    | or2list (t as Const ("HOL.eq",_) $ _ $ _) = TermC.list2isalist HOLogic.boolT [t]
    1.29    | or2list ors =
    1.30      let
    1.31 @@ -115,7 +107,7 @@
    1.32  (*>val t = @{term True};
    1.33  > val t' = or2list t;
    1.34  > term2str t';
    1.35 -"Prog_Expr.UniversalList"
    1.36 +"ListC.UniversalList"
    1.37  > val t = @{term False};
    1.38  > val t' = or2list t;
    1.39  > term2str t';