(* collect all knowledge defined in theories so far

   author: Walther Neuper 0003

   (c) isac-team

use"Knowledge/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 ListC.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");