1.1 --- a/src/Tools/isac/BaseDefinitions/termC.sml	Wed Jan 11 11:38:01 2023 +0100
     1.2 +++ b/src/Tools/isac/BaseDefinitions/termC.sml	Wed Jan 25 15:52:33 2023 +0100
     1.3 @@ -103,13 +103,14 @@
     1.4    val sym_trm : term -> term (* unused code, kept as hints to design ideas *)
     1.5  
     1.6    val string_of_detail: Proof.context -> term -> string
     1.7 +(*from isac_test for Minisubpbl*)
     1.8 +  val atom_typ: Proof.context -> typ -> unit
     1.9  
    1.10  \<^isac_test>\<open>
    1.11    val mk_negative: typ -> term -> term
    1.12    val mk_Var: term -> term
    1.13    val scala_of_term: term -> string
    1.14  
    1.15 -  val atom_typ: Proof.context -> typ -> unit
    1.16    val atom_write: Proof.context -> term -> unit
    1.17    val atom_trace: Proof.context -> term -> unit
    1.18  
    1.19 @@ -190,6 +191,7 @@
    1.20        scala_of_term t)
    1.21    | scala_of_term (t1 $ t2) =
    1.22      enclose "App(" ")" (scala_of_term t1 ^ ", " ^ scala_of_term t2)
    1.23 +\<close>
    1.24  
    1.25  (* see structure's bare bones.
    1.26     for Isabelle standard output compare 2017 "structure ML_PP" *)
    1.27 @@ -204,6 +206,8 @@
    1.28        | atol n (T :: Ts) = (ato n T ^ atol n Ts)
    1.29  in tracing (ato 0 t ^ "\n") end;
    1.30  
    1.31 +
    1.32 +\<^isac_test>\<open>
    1.33  local 
    1.34    fun ato (Const (a, _)) n = "\n*** " ^ indent n ^ "Const (" ^ a ^ ", _)"
    1.35  	  | ato (Free (a, _)) n = "\n*** " ^ indent n ^ "Free (" ^ a ^ ", _)"
    1.36 @@ -525,7 +529,7 @@
    1.37    | NONE => raise TERM ("NO parseNEW'' for " ^ str, [])
    1.38  (*\----- old versions to be eliminated -------------------------------------------------------/*)
    1.39  
    1.40 -(* to be replaced by parse..*)
    1.41 +(* to be replaced by Syntax.read_term..*)
    1.42  fun parse ctxt str = Syntax.read_term_global (Proof_Context.theory_of ctxt) str;
    1.43  (* parse term patterns; Var ("v",_), i.e. "?v", are required for instantiation *)
    1.44  fun parse_patt thy str = (thy, str)