1.1 --- a/src/Tools/isac/Knowledge/Build_Thydata.thy	Thu Jun 19 08:12:08 2014 +0200
     1.2 +++ b/src/Tools/isac/Knowledge/Build_Thydata.thy	Thu Jun 19 08:15:50 2014 +0200
     1.3 @@ -7,31 +7,6 @@
     1.4    Test_Build_Thydata (*for test/../build_thydata.sml, thy_hierarchy.sml*)
     1.5  begin
     1.6  
     1.7 -ML {*
     1.8 -  (*writeln ("======= length (KEStore_Elems = " ^
     1.9 -    (KEStore_Elems.get_mets @{theory} |> count_kestore_ptyps |> string_of_int));
    1.10 -  writeln ("======= length (! mets) = " ^
    1.11 -    (count_kestore_ptyps (! mets) |> string_of_int));
    1.12 -
    1.13 -  (* when creating session Isac see output in ~/.isabelle/../log/Isac *)
    1.14 -  writeln "======= begin KEStore_Elems.get_mets @{theory} =======";
    1.15 -  KEStore_Elems.get_mets @{theory} |> map check_kestore_met;
    1.16 -  KEStore_Elems.get_mets @{theory}
    1.17 -    |> map check_kestore_met |> map writeln;
    1.18 -  writeln "\n\n======= KEStore_Elems.get_mets @{theory} ordered =======";
    1.19 -  KEStore_Elems.get_mets @{theory} |> sort_kestore_met |> sort ptyp_ord
    1.20 -    |> map check_kestore_met |> enumerate_strings |> sort string_ord |> map writeln;
    1.21 -  writeln "======= end KEStore_Elems.get_mets @{theory} =======";
    1.22 -
    1.23 -  (* use a diff-tool for comparing KEStore_Elems.get_cas <--> ! xxx *)
    1.24 -  writeln "======= begin ! mets =======";
    1.25 -  ! mets |> map check_kestore_met |> map writeln;
    1.26 -  writeln "\n\n======= ! mets ordered =======";
    1.27 -  ! mets |> sort_kestore_met |> sort ptyp_ord
    1.28 -    |> map check_kestore_met |> enumerate_strings |> sort string_ord |> map writeln;
    1.29 -  writeln "======= end ! mets =======";*)
    1.30 -*}
    1.31 -
    1.32  subsection {* Build <Theory>-Data *}
    1.33  text {*
    1.34    <Theory>-Data represent Isac's "deductive knowledge" (whereas <Problems> and <Methods> 

     2.1 --- a/src/Tools/isac/calcelems.sml	Thu Jun 19 08:12:08 2014 +0200
     2.2 +++ b/src/Tools/isac/calcelems.sml	Thu Jun 19 08:15:50 2014 +0200
     2.3 @@ -879,23 +879,22 @@
     2.4  		      "consider setting 'check_guhs_unique := false'")
     2.5      else ();
     2.6  
     2.7 -fun insrt _ pbt [k] [] = [Ptyp (k, [pbt],[])]
     2.8 -  | insrt d pbt [k] ((Ptyp (k', [p], ps))::pys) =
     2.9 -((*tracing("### insert 1: ks = "^(strs2str [k])^"    k'= "^k');*)
    2.10 -     if k=k'
    2.11 -     then ((Ptyp (k', [pbt], ps))::pys)
    2.12 -     else (*ev.newly added pbt is free _only_ with 'last_elem pblID'*)
    2.13 -	 ((Ptyp (k', [p], ps))::(insrt d pbt [k] pys))
    2.14 -)			 
    2.15 +fun insrt _ pbt [k] [] = [Ptyp (k, [pbt], [])]
    2.16 +  | insrt d pbt [k] ((Ptyp (k', [p], ps)) :: pys) =
    2.17 +      ((*writeln ("### insert 1: ks = " ^ strs2str [k] ^ "    k'= " ^ k');*)
    2.18 +      if k = k'
    2.19 +      then ((Ptyp (k', [pbt], ps)) :: pys)
    2.20 +      else  ((Ptyp (k', [p], ps)) :: (insrt d pbt [k] pys))
    2.21 +      )			 
    2.22    | insrt d pbt (k::ks) ((Ptyp (k', [p], ps))::pys) =
    2.23 -((*tracing("### insert 2: ks = "^(strs2str (k::ks))^"    k'= "^k');*)
    2.24 -     if k=k'
    2.25 -     then ((Ptyp (k', [p], insrt d pbt ks ps))::pys)
    2.26 -     else 
    2.27 -	 if length pys = 0
    2.28 -	 then error ("insert: not found "^(strs2str (d:pblID)))
    2.29 -	 else ((Ptyp (k', [p], ps))::(insrt d pbt (k::ks) pys))
    2.30 -);
    2.31 +      ((*writeln ("### insert 2: ks = "^(strs2str (k::ks))^"    k'= "^k');*)
    2.32 +      if k = k'
    2.33 +      then ((Ptyp (k', [p], insrt d pbt ks ps)) :: pys)
    2.34 +      else 
    2.35 +        if length pys = 0
    2.36 +        then error ("insert: not found " ^ (strs2str (d : pblID)))
    2.37 +        else ((Ptyp (k', [p], ps)) :: (insrt d pbt (k :: ks) pys))
    2.38 +      );
    2.39  
    2.40  fun update_ptyps ID _ _ [] =
    2.41      error ("update_ptyps: " ^ strs2str' ID ^ " does not exist")