src/Tools/isac/BaseDefinitions/termC.sml
changeset 60565 f92963a33fe3
parent 60564 90ea835c07b3
child 60567 bb3140a02f3d
     1.1 --- a/src/Tools/isac/BaseDefinitions/termC.sml	Sun Oct 09 06:53:03 2022 +0200
     1.2 +++ b/src/Tools/isac/BaseDefinitions/termC.sml	Sun Oct 09 07:44:22 2022 +0200
     1.3 @@ -589,7 +589,7 @@
     1.4  fun parse_patt_test thy str = (thy, str)
     1.5    |>> Proof_Context.init_global
     1.6    |-> Proof_Context.read_term_pattern
     1.7 -(**)|> typ_a2real;       (** )TODO drop*)
     1.8 +  |> Model_Pattern.adapt_term_to_type (Proof_Context.init_global thy)
     1.9  fun str2term str = parse_patt (ThyC.get_theory "Isac_Knowledge") str
    1.10  
    1.11