1.1 --- a/src/Tools/isac/IsacKnowledge/Rational-WN.sml	Fri Aug 20 12:25:37 2010 +0200
     1.2 +++ b/src/Tools/isac/IsacKnowledge/Rational-WN.sml	Fri Aug 20 14:58:43 2010 +0200
     1.3 @@ -137,11 +137,11 @@
     1.4  val cT = HOLogic.realT; val vT = HOLogic.realT; val pT = HOLogic.realT;
     1.5  val eT = HOLogic.realT;
     1.6  val t = mk_mono cT vT pT eT ~5 "x" 5;
     1.7 -cterm_of (sign_of thy) t;
     1.8 +(Thm.cterm thy) t;
     1.9  val t = mk_mono cT vT pT eT ~1 "x" 0;
    1.10 -cterm_of (sign_of thy) t;
    1.11 +(Thm.cterm thy) t;
    1.12  val t = mk_mono cT vT pT eT 1 "x" 1;
    1.13 -cterm_of (sign_of thy) t;
    1.14 +(Thm.cterm thy) t;
    1.15  
    1.16  
    1.17  fun mk_sum pT t1 t2 = Const ("op +", [pT, pT]--->pT) $ t1 $ t2;
    1.18 @@ -164,21 +164,21 @@
    1.19  
    1.20  (*tests*)    
    1.21  val t = poly2term cT vT pT eT [~1] "x";
    1.22 -cterm_of (sign_of thy) t;
    1.23 +(Thm.cterm thy) t;
    1.24  val t = poly2term cT vT pT eT [0,1] "x";
    1.25 -cterm_of (sign_of thy) t;
    1.26 +(Thm.cterm thy) t;
    1.27  val t = poly2term cT vT pT eT [0,0,0,1] "x";
    1.28 -cterm_of (sign_of thy) t;
    1.29 +(Thm.cterm thy) t;
    1.30  val t = poly2term cT vT pT eT [0,0,0,3] "x";
    1.31 -cterm_of (sign_of thy) t;
    1.32 +(Thm.cterm thy) t;
    1.33  val t = poly2term cT vT pT eT [~1,0,0,3] "x";
    1.34 -cterm_of (sign_of thy) t;
    1.35 +(Thm.cterm thy) t;
    1.36  val t = poly2term cT vT pT eT [~1,0,0,3,0,5] "x";
    1.37 -cterm_of (sign_of thy) t;
    1.38 +(Thm.cterm thy) t;
    1.39  val t = poly2term cT vT pT eT [~1,0,0,3,0,5,0,7] "x";
    1.40 -cterm_of (sign_of thy) t;
    1.41 +(Thm.cterm thy) t;
    1.42  val t = poly2term cT vT pT eT [0,0,0,3,0,5,0,7] "x";
    1.43 -cterm_of (sign_of thy) t;
    1.44 +(Thm.cterm thy) t;
    1.45  
    1.46  "***************************************************************************";
    1.47  "*                            reverse-rewriting 12.8.02                    *";