src/Tools/isac/BaseDefinitions/termC.sml
changeset 60561 b6ab5b15cb52
parent 60559 aba19e46dd84
child 60564 90ea835c07b3
     1.1 --- a/src/Tools/isac/BaseDefinitions/termC.sml	Sat Oct 08 12:13:13 2022 +0200
     1.2 +++ b/src/Tools/isac/BaseDefinitions/termC.sml	Sat Oct 08 15:41:11 2022 +0200
     1.3 @@ -565,13 +565,10 @@
     1.4  fun parse_patt thy str = (thy, str)
     1.5    |>> Proof_Context.init_global
     1.6    |-> Proof_Context.read_term_pattern
     1.7 -(*|> numbers_to_string   TODO drop*)
     1.8    |> typ_a2real;       (*TODO drop*)
     1.9  fun parse_patt_PIDE thy str = (thy, str)
    1.10    |>> Proof_Context.init_global
    1.11    |-> Proof_Context.read_term_pattern
    1.12 -(*|> numbers_to_string   TODO drop*)
    1.13 -(*|> typ_a2real;         TODO drop*)
    1.14  fun str2term str = parse_patt (ThyC.get_theory "Isac_Knowledge") str
    1.15  
    1.16  fun is_atom (Const _) = true