1.1 --- a/src/Tools/isac/calcelems.sml	Wed Oct 06 14:52:12 2010 +0200
     1.2 +++ b/src/Tools/isac/calcelems.sml	Wed Oct 06 15:12:41 2010 +0200
     1.3 @@ -241,7 +241,7 @@
     1.4  val theory2theory' = string_of_thy;
     1.5  val theory2str = string_of_thy; (*WN050903 ..most consistent naming*)
     1.6  val theory2str' = implode o (drop_last_n 4) o explode o string_of_thy;
     1.7 -(*> theory2str' Isac.thy;
     1.8 +(*> theory2str' (theory "Isac");
     1.9  al it = "Isac" : string
    1.10  *)
    1.11  
    1.12 @@ -252,9 +252,9 @@
    1.13         else thyID ^ ".thy"
    1.14      end;
    1.15  (* thyID2theory' "Isac" (*ok*);
    1.16 -val it = "Isac.thy" : theory'
    1.17 - > thyID2theory' "Isac.thy" (*abuse, goes ok...*);
    1.18 -val it = "Isac.thy" : theory'
    1.19 +val it = "Isac" : theory'
    1.20 + > thyID2theory' "Isac" (*abuse, goes ok...*);
    1.21 +val it = "Isac" : theory'
    1.22  *)
    1.23  
    1.24  fun theory'2thyID (theory':theory') =
    1.25 @@ -263,7 +263,7 @@
    1.26      in if ext = ".thy" then ((implode o (drop_last_n 4)) ss) : thyID
    1.27         else theory' (*disarm abuse of theory'*)
    1.28      end;
    1.29 -(* theory'2thyID "Isac.thy";
    1.30 +(* theory'2thyID "Isac";
    1.31  val it = "Isac" : thyID
    1.32  > theory'2thyID "Isac";
    1.33  val it = "Isac" : thyID*)