1.1 --- a/src/Tools/isac/calcelems.sml	Sun Sep 13 12:37:57 2015 +0200
     1.2 +++ b/src/Tools/isac/calcelems.sml	Sun Sep 20 11:29:49 2015 +0200
     1.3 @@ -27,6 +27,9 @@
     1.4  revise funs      : id_of_thm, thm_of_thm, rep_thm_G', eq_thmI, eq_thmI', thm'_of_thm thm.
     1.5  activate         : thmID_of_derivation_name'
     1.6  *)
     1.7 +type iterID = int;
     1.8 +type calcID = int;
     1.9 +
    1.10  type thmID = string;    (* identifier for a thm (the shortest possible identifier)       *)
    1.11  type thmDeriv = string; (* WN120524 deprecated
    1.12    thyID ^"."^ xxx ^"."^ thmID, see fun thmID_of_derivation_name 
    1.13 @@ -487,6 +490,12 @@
    1.14    | str2ketype "Pbl_" = Pbl_
    1.15    | str2ketype "Met_" = Met_
    1.16    | str2ketype str = raise ERROR ("str2ketype: WRONG arg = " ^ str)
    1.17 +(* for conversion from XML *)
    1.18 +fun str2ketype' "exp" = Exp_
    1.19 +  | str2ketype' "thy" = Thy_
    1.20 +  | str2ketype' "pbl" = Pbl_
    1.21 +  | str2ketype' "met" = Met_
    1.22 +  | str2ketype' str = raise ERROR ("str2ketype': WRONG arg = " ^ str)
    1.23  
    1.24  (*rewrite orders, also stored in 'type met' and type 'and rls'
    1.25    The association list is required for 'rewrite.."rew_ord"..'