diff -r a28b5fc129b7 -r 22235e4dbe5f src/Tools/isac/IsacKnowledge/Isac.ML
--- a/src/Tools/isac/IsacKnowledge/Isac.ML	Wed Aug 25 15:15:01 2010 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,37 +0,0 @@
-(* collect all knowledge defined in theories so far
-   author: Walther Neuper 0003
-   (c) isac-team
-
-use"IsacKnowledge/Isac.ML";
-use"Isac.ML";
- *)
-
-
-theory' := overwritel (!theory', [("Isac.thy",Isac.thy)]);
-
-
-(**.set up a list for getting guh + theID for a thm (defined in isabelle).**)
-
-(*.get all theorems used by isac and defined in isabelle.*)
-local
-    val isacrlsthms = ((gen_distinct eq_thmI) o (map rep_thm_G') o flat o 
-		       (map (thms_of_rls o #2 o #2))) (!ruleset');
-    val isacthms = (flat o (map (PureThy.all_thms_of o #2))) (!theory');
-in
-    val rlsthmsNOTisac = gen_diff eq_thmI (isacrlsthms, isacthms);
-end;
-
-(*.set up the list using 'val first_isac_thy' (see ListG.ML).*)
-isab_thm_thy := make_isab rlsthmsNOTisac
-			  ((#ancestors o rep_theory) first_isac_thy);
-
-
-(*.create the hierarchy of theory elements from IsacKnowledge
-   including thms from Isabelle used in rls;
-   elements store_*d in any *.ML are not overwritten.*)
-
-thehier := the_hier (!thehier) (collect_thydata ());
-writeln("----------------------------------\n\
-	\*** insert: not found ... IS OK : \n\
-	\comes from fill_parents           \n\
-	\----------------------------------\n");