1.1 --- a/src/Tools/isac/Knowledge/Rational-WN.sml	Mon Sep 27 13:35:06 2010 +0200
     1.2 +++ b/src/Tools/isac/Knowledge/Rational-WN.sml	Tue Sep 28 07:28:10 2010 +0200
     1.3 @@ -20,7 +20,7 @@
     1.4  ---------------------------------------------------------------------*)
     1.5  
     1.6  
     1.7 -(*diese vvv funktionen kommen nach src/Isa99/term.sml -------------*)
     1.8 +(*diese vvv funktionen kommen nach src/Isa99/termC.sml -------------*)
     1.9  fun term2str t =
    1.10      let fun ato (Const(a,T))     n = 
    1.11  	    "\n"^indent n^"Const ( "^a^")"
    1.12 @@ -37,7 +37,7 @@
    1.13  fun free2int (t as Free (s, _)) = (((the o int_of_str) s)
    1.14      handle _ => raise error ("free2int: "^term2str t))
    1.15    | free2int t = raise error ("free2int: "^term2str t);
    1.16 -(*diese ^^^ funktionen kommen nach src/Isa99/term.sml -------------*)
    1.17 +(*diese ^^^ funktionen kommen nach src/Isa99/termC.sml -------------*)
    1.18  
    1.19  
    1.20  (* remark on exceptions: 'error' is implemented by Isabelle