1.1 --- a/src/Tools/isac/Knowledge/Rational-WN.sml Mon Dec 07 10:01:49 2015 +0100
1.2 +++ b/src/Tools/isac/Knowledge/Rational-WN.sml Mon Dec 07 10:17:08 2015 +0100
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 thy) t;
1.8 +(Thm.global_cterm_of thy) t;
1.9 val t = mk_mono cT vT pT eT ~1 "x" 0;
1.10 -(cterm_of thy) t;
1.11 +(Thm.global_cterm_of thy) t;
1.12 val t = mk_mono cT vT pT eT 1 "x" 1;
1.13 -(cterm_of thy) t;
1.14 +(Thm.global_cterm_of thy) t;
1.15
1.16
1.17 fun mk_sum pT t1 t2 = Const ("Groups.plus_class.plus", [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 thy) t;
1.23 +(Thm.global_cterm_of thy) t;
1.24 val t = poly2term cT vT pT eT [0,1] "x";
1.25 -(cterm_of thy) t;
1.26 +(Thm.global_cterm_of thy) t;
1.27 val t = poly2term cT vT pT eT [0,0,0,1] "x";
1.28 -(cterm_of thy) t;
1.29 +(Thm.global_cterm_of thy) t;
1.30 val t = poly2term cT vT pT eT [0,0,0,3] "x";
1.31 -(cterm_of thy) t;
1.32 +(Thm.global_cterm_of thy) t;
1.33 val t = poly2term cT vT pT eT [~1,0,0,3] "x";
1.34 -(cterm_of thy) t;
1.35 +(Thm.global_cterm_of thy) t;
1.36 val t = poly2term cT vT pT eT [~1,0,0,3,0,5] "x";
1.37 -(cterm_of thy) t;
1.38 +(Thm.global_cterm_of thy) t;
1.39 val t = poly2term cT vT pT eT [~1,0,0,3,0,5,0,7] "x";
1.40 -(cterm_of thy) t;
1.41 +(Thm.global_cterm_of thy) t;
1.42 val t = poly2term cT vT pT eT [0,0,0,3,0,5,0,7] "x";
1.43 -(cterm_of thy) t;
1.44 +(Thm.global_cterm_of thy) t;
1.45
1.46 "***************************************************************************";
1.47 "* reverse-rewriting 12.8.02 *";