1.1 --- a/src/Tools/isac/BaseDefinitions/unparseC.sml	Wed Jan 11 06:06:12 2023 +0100
     1.2 +++ b/src/Tools/isac/BaseDefinitions/unparseC.sml	Wed Jan 11 09:23:18 2023 +0100
     1.3 @@ -27,12 +27,8 @@
     1.4  
     1.5  (*val terms_short: Proof.context -> term list -> term_as_string*)
     1.6    val terms_short: term list -> term_as_string
     1.7 -
     1.8  (*val typ: Proof.context -> typ -> term_as_string*)
     1.9    val typ_in_ctxt: Proof.context -> typ -> term_as_string
    1.10 -  val typ: typ -> term_as_string
    1.11 -(*replace by ^^^*)
    1.12 -  val typ_by_thyID: ThyC.id -> typ -> term_as_string
    1.13  
    1.14  \<^isac_test>\<open>
    1.15    val term_by_thyID: ThyC.id -> term -> term_as_string
    1.16 @@ -76,16 +72,6 @@
    1.17  fun term_opt (SOME t) = "(SOME " ^ term t ^ ")"
    1.18    | term_opt NONE = "NONE";
    1.19  
    1.20 -fun type_to_string'' (thyID : ThyC.id) t =
    1.21 -  let
    1.22 -    val ctxt' = Config.put show_markup false (Proof_Context.init_global
    1.23 -      (ThyC.get_theory thyID))
    1.24 -  in
    1.25 -    Print_Mode.setmp [] (Syntax.string_of_typ ctxt') t
    1.26 -  end;
    1.27 -fun typ typ = type_to_string'' "Isac_Knowledge" typ; (*TODO legacy*)
    1.28 -fun typ_by_thyID thy typ = type_to_string'' thy typ; (*legacy*)
    1.29 -
    1.30  fun type_to_string' ctxt typ =
    1.31    Print_Mode.setmp [] (Syntax.string_of_typ ctxt) typ
    1.32  fun typ_in_ctxt ctxt typ = type_to_string' ctxt typ