src/Tools/isac/Knowledge/DiffApp-oldpbl.sml
changeset 59186 d9c3e373f8f5
parent 37947 22235e4dbe5f
child 59377 9d7115bbdb01
     1.1 --- a/src/Tools/isac/Knowledge/DiffApp-oldpbl.sml	Mon Dec 07 10:52:07 2015 +0100
     1.2 +++ b/src/Tools/isac/Knowledge/DiffApp-oldpbl.sml	Mon Dec 07 11:25:02 2015 +0100
     1.3 @@ -330,7 +330,7 @@
     1.4  (*
     1.5  {given=[],where_=[],find=[],with_=[],relate=[]}: string ppc;
     1.6  val (SOME ct) = parse thy ;
     1.7 -atomty thy (term_of ct);
     1.8 +atomty thy (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 ppc;
    1.15  val (SOME ct) = parse thy ;
    1.16 -atomty thy (term_of ct);
    1.17 +atomty thy (Thm.term_of ct);
    1.18  *)