1.1 --- a/src/Tools/isac/BaseDefinitions/termC.sml	Sun Apr 18 22:27:43 2021 +0200
     1.2 +++ b/src/Tools/isac/BaseDefinitions/termC.sml	Sun Apr 18 23:37:59 2021 +0200
     1.3 @@ -94,7 +94,7 @@
     1.4    val dest_list': term -> term list
     1.5    val negates: term -> term -> bool
     1.6  
     1.7 -(* ---- for tests only: shifted from below to remove the Warning "unused" at fun.def. --------- *)
     1.8 +\<^isac_test>\<open>
     1.9    val scala_of_term: term -> string
    1.10    val atomtyp(*<-- atom_typ TODO*): typ -> unit
    1.11    val atomty: term -> unit
    1.12 @@ -103,12 +103,10 @@
    1.13    val atomwy: term -> unit
    1.14    val atomty_thy: ThyC.id -> term -> unit
    1.15    val free2var: term -> term
    1.16 +  val typ_a2real: term -> term
    1.17 +\<close>
    1.18    val contains_one_of: thm * (string * typ) list -> bool
    1.19    val contains_Const_typeless: term list -> term -> bool
    1.20 -(*/-------------------------------------------------------- ! aktivate for Test_Isac BEGIN ---\* )
    1.21 -  val typ_a2real: term -> term
    1.22 -( *\--- ! aktivate for Test_Isac END ----------------------------------------------------------/*)
    1.23 -
    1.24  (*----- unused code, kept as hints to design ideas ---------------------------------------------*)
    1.25    val sym_trm : term -> term
    1.26  end
    1.27 @@ -146,6 +144,7 @@
    1.28  
    1.29  (** transform  typ / term to a String to be parsed by Scala after transport via libisabelle **)
    1.30  
    1.31 +\<^isac_test>\<open>
    1.32  fun scala_of_typ (Type (s, typs)) =
    1.33      enclose "Type(" ")" (quote s ^ ", " ^
    1.34        (typs |> map scala_of_typ |> commas |> enclose "List(" ")"))
    1.35 @@ -155,6 +154,7 @@
    1.36      enclose "TVar(" ")" (
    1.37        enclose "(" ")," (quote s ^ ", " ^ quote (string_of_int i)) ^ 
    1.38        (sort |> map quote |> commas |> enclose "List(" ")"))
    1.39 +
    1.40  fun scala_of_term (Const (s, T)) =
    1.41      enclose "Const(" ")" (quote s ^ ", " ^ scala_of_typ T)
    1.42    | scala_of_term (Free (s, T)) =
    1.43 @@ -197,6 +197,7 @@
    1.44    fun atomw t = writeln ("\n*** -------------" ^ ato t 0 ^ "\n***");
    1.45    fun atomt t = tracing ("\n*** -------------" ^ ato t 0 ^ "\n***");
    1.46  end;
    1.47 +\<close>
    1.48  
    1.49  fun term_detail2str t =
    1.50    let 
    1.51 @@ -209,6 +210,8 @@
    1.52          "\n*** " ^ indent n ^ "Abs (" ^ a ^ ", " ^ UnparseC.typ T ^ ",.." ^ ato body (n + 1)
    1.53        | ato (f $ t) n = ato f n ^ ato t (n + 1)
    1.54    in "\n*** " ^ ato t 0 ^ "\n***" end;
    1.55 +
    1.56 +\<^isac_test>\<open>
    1.57  fun term_detail2str_thy thy t =
    1.58    let
    1.59      fun ato (Const (a, T)) n =
    1.60 @@ -228,6 +231,7 @@
    1.61  fun atomwy t = (writeln o term_detail2str) t;
    1.62  fun atomty t = (tracing o term_detail2str) t;
    1.63  fun atomty_thy thy t = (tracing o (term_detail2str_thy thy)) t;
    1.64 +\<close>
    1.65  
    1.66  (* contains the term a VAR(("*",_),_) ? *)
    1.67  fun contains_Var (Abs(_,_,body)) = contains_Var body
    1.68 @@ -321,6 +325,7 @@
    1.69    | var2free (Abs(s, T, t)) = Abs(s, T, var2free t)
    1.70    | var2free (t1 $ t2) = (var2free t1) $ (var2free t2);
    1.71    
    1.72 +\<^isac_test>\<open>
    1.73  (* Logic.varify does NOT take care of 'Free ("1", _)'*)
    1.74  fun free2var (t as Const _) = t
    1.75    | free2var (t as Free (s, T)) = if is_num' s then t else Var ((s, 0), T)
    1.76 @@ -328,6 +333,7 @@
    1.77    | free2var (t as Bound _) = t 
    1.78    | free2var (Abs (s, T, t)) = Abs (s, T, free2var t)
    1.79    | free2var (t1 $ t2) = (free2var t1) $ (free2var t2);
    1.80 +\<close>
    1.81  
    1.82  fun mk_listT T = Type ("List.list", [T]);
    1.83  fun list_const T = Const ("List.list.Cons", [T, mk_listT T] ---> mk_listT T);