1.1 --- a/src/Tools/isac/ProgLang/termC.sml	Wed Jul 31 09:46:50 2019 +0200
     1.2 +++ b/src/Tools/isac/ProgLang/termC.sml	Fri Aug 09 14:04:13 2019 +0200
     1.3 @@ -4,7 +4,8 @@
     1.4  *)
     1.5  infix contains_one_of
     1.6  
     1.7 -signature TERMC =
     1.8 +(* TERM_C extends Isabelle's naming conventions: "C" indicates Isac add-ons to an Isabelle module *)
     1.9 +signature TERM_C =
    1.10    sig
    1.11      val contains_Var: term -> bool
    1.12      val dest_binop_typ: typ -> typ * typ * typ
    1.13 @@ -71,6 +72,7 @@
    1.14      val var2free: term -> term
    1.15      val vars: term -> term list
    1.16      val vars_of : term -> term list (* probably should replace "fun vars" *)
    1.17 +    val dest_list' : term -> term list
    1.18  
    1.19  (* ---- for tests only: shifted from below to remove the Warning "unused" at fun.def. --------- *)
    1.20      val scala_of_term: term -> string
    1.21 @@ -88,7 +90,7 @@
    1.22    end
    1.23  
    1.24  (**)
    1.25 -structure TermC(**): TERMC(**) =
    1.26 +structure TermC(**): TERM_C(**) =
    1.27  struct
    1.28  (**)
    1.29  
    1.30 @@ -546,4 +548,8 @@
    1.31      val var_ids = t |> ids2str |> subtract op = poly_consts |> map strip_thy |> sort string_ord
    1.32    in (map (var_for [] t) var_ids) |> flat |> distinct end
    1.33  
    1.34 +(* this may decompose an object-language isa-list;
    1.35 +   use only, if description is not available, eg. not input ?WN:14.5.03 ??!?*)
    1.36 +fun dest_list' t = if is_list t then isalist2list t  else [t];
    1.37 +
    1.38  end
    1.39 \ No newline at end of file