1.1 --- a/test/Tools/isac/Knowledge/biegelinie.sml	Tue Aug 31 16:00:13 2010 +0200
     1.2 +++ b/test/Tools/isac/Knowledge/biegelinie.sml	Tue Aug 31 16:38:22 2010 +0200
     1.3 @@ -145,9 +145,9 @@
     1.4  				   Calc("op +", eval_binop "#add_")
     1.5  				   ], 
     1.6  		srls = Erls, calc = [],
     1.7 -		rules = [Thm ("nth_Cons_",num_str nth_Cons_),
     1.8 +		rules = [Thm ("nth_Cons_",num_str @{nth_Cons_),
     1.9  			 Calc("op +", eval_binop "#add_"),
    1.10 -			 Thm ("nth_Nil_",num_str nth_Nil_),
    1.11 +			 Thm ("nth_Nil_",num_str @{nth_Nil_),
    1.12  			 Calc("Tools.lhs", eval_lhs"eval_lhs_"),
    1.13  			 Calc("Tools.rhs", eval_rhs"eval_rhs_"),
    1.14  			 Calc("Atools.argument'_in",
    1.15 @@ -1012,9 +1012,9 @@
    1.16  val srls = append_rls "erls_IntegrierenUndK.." e_rls 
    1.17  		      [Calc("Tools.rhs", eval_rhs"eval_rhs_"),
    1.18  		       Calc ("Atools.ident",eval_ident "#ident_"),
    1.19 -		       Thm ("last_thmI",num_str last_thmI),
    1.20 -		       Thm ("if_True",num_str if_True),
    1.21 -		       Thm ("if_False",num_str if_False)
    1.22 +		       Thm ("last_thmI",num_str @{last_thmI),
    1.23 +		       Thm ("if_True",num_str @{if_True),
    1.24 +		       Thm ("if_False",num_str @{if_False)
    1.25  		       ]
    1.26  		      ;
    1.27  val t = str2term "last [1,2,3,4]";