diff -r 15775bd26979 -r 10a171ce75d5 src/Tools/isac/calcelems.sml
--- a/src/Tools/isac/calcelems.sml	Fri Sep 10 10:36:41 2010 +0200
+++ b/src/Tools/isac/calcelems.sml	Fri Sep 10 11:58:46 2010 +0200
@@ -150,6 +150,9 @@
 fun rep_thm_G' (Thm (thmid, thm)) = (thmid, thm);
 fun eq_thmI ((thmid1 : thmID, _ : thm), (thmid2 : thmID, _ : thm)) =
     (strip_thy thmid1) = (strip_thy thmid2);
+(*version typed weaker WN100910*)
+fun eq_thmI' ((thmid1, _), (thmid2, _)) =
+    (strip_thy thmid1) = (strip_thy thmid2);
 
 
 val string_of_thm =  Thm.get_name_hint; (*FIXME.2009*)
@@ -382,7 +385,7 @@
 		 | Hthm of {guh: guh,
 			    coursedesign: authors,
 			    mathauthors: authors,
-			    thm: Thm.thm}
+			    thm: term}
 		 | Hrls of {guh: guh,
 			    coursedesign: authors,
 			    mathauthors: authors,
@@ -403,7 +406,7 @@
 val thehier = ref ([] : thehier);
 
 (*.an association list, gets the value once in Isac.ML.*)
-val isab_thm_thy = ref ([] : (thmID * (thyID * thm)) list);
+val isab_thm_thy = ref ([] : (thmID * (thyID * term)) list);
 
 
 type path = string;