Mercurial Mercurial > wneuper > isa / diff
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
src/Tools/isac/BaseDefinitions/termC.sml
changeset 60586 007ef64dbb08
parent 60585 b7071d1dd263
child 60649 b2ff1902420f 
     1.1 --- a/src/Tools/isac/BaseDefinitions/termC.sml	Mon Oct 31 18:28:36 2022 +0100
     1.2 +++ b/src/Tools/isac/BaseDefinitions/termC.sml	Mon Nov 07 17:37:20 2022 +0100
     1.3 @@ -551,7 +551,7 @@
     1.4  (** parse in test/* **)
     1.5  (*
     1.6    This bypasses building ctxt at the begin of a calculation
     1.7 -  and thus borrows adapt_to_type (used for pre-parsed terms from Know_Store).
     1.8 +  and thus borrows adapt_to_type (used for where_-parsed terms from Know_Store).
     1.9  *)
    1.10  fun parse_test ctxt str = str 
    1.11    |> Syntax.read_term_global (Proof_Context.theory_of ctxt)
wneuper/isa