src/Tools/isac/BaseDefinitions/termC.sml
changeset 60567 bb3140a02f3d
parent 60565 f92963a33fe3
child 60573 7ab2b7aff287
     1.1 --- a/src/Tools/isac/BaseDefinitions/termC.sml	Sun Oct 09 09:01:29 2022 +0200
     1.2 +++ b/src/Tools/isac/BaseDefinitions/termC.sml	Wed Oct 19 10:43:04 2022 +0200
     1.3 @@ -83,7 +83,6 @@
     1.4    (*for test/* *)
     1.5  (*goal*)val parse_test: Proof.context -> string -> term
     1.6  (*goal*)val parse_patt_test: theory -> string -> term
     1.7 -  val str2term: string -> term (*to be replaced by parse/_patt in src*, by parse/_patt in test/**)
     1.8  
     1.9    val str_of_free_opt: term -> string option
    1.10    val str_of_int: int -> string
    1.11 @@ -590,7 +589,6 @@
    1.12    |>> Proof_Context.init_global
    1.13    |-> Proof_Context.read_term_pattern
    1.14    |> Model_Pattern.adapt_term_to_type (Proof_Context.init_global thy)
    1.15 -fun str2term str = parse_patt (ThyC.get_theory "Isac_Knowledge") str
    1.16  
    1.17  
    1.18  fun is_atom (Const _) = true