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