1.1 --- a/src/Tools/isac/calcelems.sml	Fri Sep 10 10:36:41 2010 +0200
     1.2 +++ b/src/Tools/isac/calcelems.sml	Fri Sep 10 11:58:46 2010 +0200
     1.3 @@ -150,6 +150,9 @@
     1.4  fun rep_thm_G' (Thm (thmid, thm)) = (thmid, thm);
     1.5  fun eq_thmI ((thmid1 : thmID, _ : thm), (thmid2 : thmID, _ : thm)) =
     1.6      (strip_thy thmid1) = (strip_thy thmid2);
     1.7 +(*version typed weaker WN100910*)
     1.8 +fun eq_thmI' ((thmid1, _), (thmid2, _)) =
     1.9 +    (strip_thy thmid1) = (strip_thy thmid2);
    1.10  
    1.11  
    1.12  val string_of_thm =  Thm.get_name_hint; (*FIXME.2009*)
    1.13 @@ -382,7 +385,7 @@
    1.14  		 | Hthm of {guh: guh,
    1.15  			    coursedesign: authors,
    1.16  			    mathauthors: authors,
    1.17 -			    thm: Thm.thm}
    1.18 +			    thm: term}
    1.19  		 | Hrls of {guh: guh,
    1.20  			    coursedesign: authors,
    1.21  			    mathauthors: authors,
    1.22 @@ -403,7 +406,7 @@
    1.23  val thehier = ref ([] : thehier);
    1.24  
    1.25  (*.an association list, gets the value once in Isac.ML.*)
    1.26 -val isab_thm_thy = ref ([] : (thmID * (thyID * thm)) list);
    1.27 +val isab_thm_thy = ref ([] : (thmID * (thyID * term)) list);
    1.28  
    1.29  
    1.30  type path = string;