1.1 --- a/src/Tools/isac/Interpret/rewtools.sml	Wed Sep 01 09:56:09 2010 +0200
     1.2 +++ b/src/Tools/isac/Interpret/rewtools.sml	Wed Sep 01 15:17:43 2010 +0200
     1.3 @@ -217,7 +217,7 @@
     1.4    | sym_Thm (Rls_ rls) = Rls_ (*WN060825?!?*) (sym_rls rls)
     1.5    | sym_Thm r = raise error ("sym_Thm: not for "^(rule2str r));
     1.6  (*
     1.7 -  val th =  Thm ("real_one_collect",num_str @{real_one_collect);
     1.8 +  val th =  Thm ("real_one_collect",num_str @{thm real_one_collect});
     1.9    sym_Thm th;
    1.10  val th =
    1.11    Thm ("real_one_collect","?m is_const ==> ?n + ?m * ?n = (1 + ?m) * ?n")