src/Tools/isac/Knowledge/DiffApp-oldpbl.sml
changeset 60650 06ec8abfd3bc
parent 60586 007ef64dbb08
     1.1 --- a/src/Tools/isac/Knowledge/DiffApp-oldpbl.sml	Wed Jan 11 09:23:18 2023 +0100
     1.2 +++ b/src/Tools/isac/Knowledge/DiffApp-oldpbl.sml	Wed Jan 11 11:38:01 2023 +0100
     1.3 @@ -330,7 +330,7 @@
     1.4  (*
     1.5  {given=[],where_=[],find=[],with_=[],relate=[]}: string model;
     1.6  val (SOME ct) = parse thy ;
     1.7 -atomty thy (Thm.term_of ct);
     1.8 +TermC.atom_trace_detail @{context} (Thm.term_of ct);
     1.9  *)
    1.10  
    1.11  
    1.12 @@ -365,5 +365,5 @@
    1.13  (*
    1.14  {given=[],where_=[],find=[],with_=[],relate=[]}: string model;
    1.15  val (SOME ct) = parse thy ;
    1.16 -atomty thy (Thm.term_of ct);
    1.17 +TermC.atom_trace_detail @{context} (Thm.term_of ct);
    1.18  *)