1.1 --- a/src/Tools/isac/BaseDefinitions/termC.sml	Wed Apr 15 11:37:43 2020 +0200
     1.2 +++ b/src/Tools/isac/BaseDefinitions/termC.sml	Wed Apr 15 13:47:56 2020 +0200
     1.3 @@ -99,7 +99,7 @@
     1.4    val atomw: term -> unit
     1.5    val atomt: term -> unit
     1.6    val atomwy: term -> unit
     1.7 -  val atomty_thy: ThyC.thyID -> term -> unit
     1.8 +  val atomty_thy: ThyC.id -> term -> unit
     1.9    val free2var: term -> term
    1.10    val contains_one_of: thm * (string * typ) list -> bool
    1.11    val contains_Const_typeless: term list -> term -> bool
    1.12 @@ -508,11 +508,11 @@
    1.13    WN130613 probably compare to 
    1.14    http://www.mail-archive.com/isabelle-dev@mailbroy.informatik.tu-muenchen.de/msg04249.html*)
    1.15  fun parse_patt thy str = (thy, str)
    1.16 -  |>> ThyC.thy2ctxt 
    1.17 +  |>> ThyC.to_ctxt 
    1.18    |-> Proof_Context.read_term_pattern
    1.19    |> numbers_to_string (*TODO drop*)
    1.20    |> typ_a2real;       (*TODO drop*)
    1.21 -fun str2term str = parse_patt (ThyC.Thy_Info_get_theory "Isac_Knowledge") str
    1.22 +fun str2term str = parse_patt (ThyC.get_theory "Isac_Knowledge") str
    1.23  
    1.24  (* TODO decide with Test_Isac *)
    1.25  fun is_atom t = length (vars t) = 1