1.1 --- a/src/Tools/isac/Knowledge/DiffApp-scrpbl.sml	Mon Dec 07 10:52:07 2015 +0100
     1.2 +++ b/src/Tools/isac/Knowledge/DiffApp-scrpbl.sml	Mon Dec 07 11:25:02 2015 +0100
     1.3 @@ -141,7 +141,7 @@
     1.4  (*
     1.5  {given=[],where_=[],find=[],with_=[],relate=[]}: string ppc;
     1.6  val (SOME ct) = parse thy ;
     1.7 -atomty (term_of ct);
     1.8 +atomty (Thm.term_of ct);
     1.9  *)
    1.10  
    1.11  
    1.12 @@ -211,14 +211,14 @@
    1.13  	      "{(a//#2)^^^#2 + (b//#2)^^^#2 = (R//#2)^^^#2}",
    1.14  	      "{R::real}"];
    1.15  val tag__forms = chktyps thy (formals, givens);
    1.16 -map ((atomty) o term_of) tag__forms;
    1.17 +map ((atomty) o Thm.term_of) tag__forms;
    1.18  
    1.19  val formals = map (the o (parse thy)) ["A=#2*a*b - a^^^#2",
    1.20  	      "alpha::real","{alpha. #0<alpha & alpha<pi//#2}",
    1.21  	      "{a//#2 = R*(sin alpha), b//#2 = R*(cos alpha)}",
    1.22  	      "{R::real}"];
    1.23  val tag__forms = chktyps thy (formals, givens);
    1.24 -map ((atomty) o term_of) tag__forms;
    1.25 +map ((atomty) o Thm.term_of) tag__forms;
    1.26  *)
    1.27  
    1.28  " --- subproblem: make-function-by-subst --- ";
    1.29 @@ -236,7 +236,7 @@
    1.30  val givens = map (the o (parse thy)) given;
    1.31  (* 5.3.00
    1.32  val tag__forms = chktyps thy (formals, givens);
    1.33 -map ((atomty) o term_of) tag__forms;
    1.34 +map ((atomty) o Thm.term_of) tag__forms;
    1.35  *)
    1.36  " --- subproblem: max-of-function --- ";
    1.37  val origin = ["A = #2*(#2*R*(sin alpha))*(#2*R*(sin alpha)) - \
    1.38 @@ -255,7 +255,7 @@
    1.39  val givens = map (the o (parse thy)) given;
    1.40  (* 5.3.00
    1.41  val tag__forms = chktyps thy (formals, givens);
    1.42 -map ((atomty) o term_of) tag__forms;
    1.43 +map ((atomty) o Thm.term_of) tag__forms;
    1.44  *)
    1.45  " --- subproblem: derivative --- ";
    1.46  val origin = ["x^^^#3-y^^^#3+#-3*x+#12*y+#10","x::real"];
    1.47 @@ -270,7 +270,7 @@
    1.48  val givens = map (the o (parse thy)) given;
    1.49  (*
    1.50  val tag__forms = chktyps thy (formals, givens);
    1.51 -map ((atomty) o term_of) tag__forms;
    1.52 +map ((atomty) o Thm.term_of) tag__forms;
    1.53  *)
    1.54  " --- subproblem: tan-quadrat-equation --- ";
    1.55  val origin = ["#8*R^^^#2*(cos alpha)^^^#2 + #-8*R^^^#2* \
    1.56 @@ -289,7 +289,7 @@
    1.57  val chkpbl = map (the o (parse thy)) (given @ where_ @ find @ with_);
    1.58  val givens = map (the o (parse thy)) given;
    1.59  val tag__forms = chktyps thy (formals, givens);
    1.60 -map ((atomty) o term_of) tag__forms;
    1.61 +map ((atomty) o Thm.term_of) tag__forms;
    1.62  *)
    1.63  (*  use"test-coil-kernel.sml";
    1.64    *)