1.1 --- a/src/Tools/isac/calcelems.sml	Tue Mar 20 15:32:17 2012 +0100
     1.2 +++ b/src/Tools/isac/calcelems.sml	Thu Apr 05 11:31:56 2012 +0200
     1.3 @@ -348,10 +348,10 @@
     1.4  (*see 'How to manage theorys in subproblems' at 'type thyID'*)
     1.5  val theory'  = Unsynchronized.ref ([]:(theory' * theory) list);
     1.6  
     1.7 -(*.all theories defined for Scripts, recorded in Scripts/Script.ML;
     1.8 -   in order to distinguish them from general IsacKnowledge defined later on.*)
     1.9 -val script_thys = Unsynchronized.ref ([] : (theory' * theory) list);
    1.10 -
    1.11 +(* theories for html representation: Isabelle, Knowledge, ProgLang *)
    1.12 +val isabthys = Unsynchronized.ref ([] : theory list);
    1.13 +val knowthys = Unsynchronized.ref ([] : theory list);
    1.14 +val progthys = Unsynchronized.ref ([] : theory list);
    1.15  
    1.16  (*rewrite orders, also stored in 'type met' and type 'and rls'
    1.17    The association list is required for 'rewrite.."rew_ord"..'
    1.18 @@ -420,7 +420,11 @@
    1.19  (* an association list, gets the value once in Isac.ML.
    1.20     stores Isabelle's thms as terms for compatibility with Theory.axioms_of.
    1.21     WN1-1-28 make this data arguments and del ref ?*)
    1.22 -val isab_thm_thy = Unsynchronized.ref ([] : (thmID * (thyID * term)) list);
    1.23 +val isab_thm_thy = Unsynchronized.ref ([] : (thmDeriv * term) list);
    1.24 +val isabthys = Unsynchronized.ref ([] : theory list);
    1.25 +
    1.26 +val first_ProgLang_thy = Unsynchronized.ref (@{theory Pure});
    1.27 +val first_Knowledge_thy = Unsynchronized.ref (@{theory Pure});
    1.28  
    1.29  
    1.30  type path = string;