1.1 --- a/test/Tools/isac/ProgLang/listC.sml	Sat Mar 10 14:53:18 2012 +0100
     1.2 +++ b/test/Tools/isac/ProgLang/listC.sml	Tue Mar 13 15:04:09 2012 +0100
     1.3 @@ -10,17 +10,17 @@
     1.4  "--------------------- nth_ ----------------------------------------------";
     1.5  val t = str2term "nth_ 3 [a,b,c,d,e]";
     1.6  atomty t;
     1.7 -val thm = (#prop o rep_thm o num_str) nth_Cons_;
     1.8 +val thm = (#prop o rep_thm o num_str) @{thm NTH_CONS};
     1.9  atomty thm;
    1.10 -val SOME (t',_) = rewrite_ thy dummy_ord Poly_erls false (num_str @{thm nth_Cons_}) t;
    1.11 +val SOME (t',_) = rewrite_ thy dummy_ord Poly_erls false (num_str @{thm NTH_CONS}) t;
    1.12  if term2str t' = "nth_ (3 + - 1) [b, c, d, e]" then () 
    1.13  else error "list_rls.sml, nth_ (3 + - 1) [b, c, d, e]";
    1.14  
    1.15  val t = str2term "nth_ 1 [a,b,c,d,e]";
    1.16  atomty t;
    1.17 -val thm = (#prop o rep_thm o num_str) nth_Nil_;
    1.18 +val thm = (#prop o rep_thm o num_str) @{thm NTH_NIL};
    1.19  atomty thm;
    1.20 -val SOME (t',_) = rewrite_ thy dummy_ord Poly_erls false (num_str @{thm nth_Nil_}) t;
    1.21 +val SOME (t',_) = rewrite_ thy dummy_ord Poly_erls false (num_str @{thm NTH_NIL}) t;
    1.22  term2str t';
    1.23  "a";
    1.24  
    1.25 @@ -33,7 +33,7 @@
    1.26  "c";
    1.27  
    1.28  (*-------------------------------------------------------------------*)
    1.29 -val SOME (Thm (_,thm)) = rls_get_thm list_rls "nth_Nil_";
    1.30 +val SOME (Thm (_,thm)) = rls_get_thm list_rls "NTH_NIL";
    1.31  val ttt = (#prop o rep_thm) thm;
    1.32  atomty ttt;
    1.33  (*Free ( 1, real)   ...OK, Var ((x, 0), ?'a) OK*)
    1.34 @@ -45,11 +45,11 @@
    1.35  "--------------------- length_ -------------------------------------------";
    1.36  val thy' = "ListG";
    1.37  val ct = "length_ [1,1,1]";
    1.38 -val thm = ("length_Cons_","");
    1.39 +val thm = (@{thm LENGTH_CONS},"");
    1.40  val (ct,asm) = the (rewrite thy' "tless_true" ("tval_rls") false thm ct);
    1.41  val (ct,asm) = the (rewrite thy' "tless_true" ("tval_rls") false thm ct);
    1.42  val (ct,asm) = the (rewrite thy' "tless_true" ("tval_rls") false thm ct);
    1.43 -val thm = ("length_Nil_","");
    1.44 +val thm = (@{thm LENGTH_NIL},"");
    1.45  val (ct,asm) = the (rewrite thy' "tless_true" ("tval_rls") false thm ct);
    1.46  if ct="1 + (1 + (1 + 0))"then()
    1.47  else error ("list_rls.sml 1: behaviour of test-expl changed: "^ct);