1.1 --- a/src/Tools/isac/KEStore.thy	Thu Jun 05 15:49:44 2014 +0200
     1.2 +++ b/src/Tools/isac/KEStore.thy	Thu Jun 05 16:41:42 2014 +0200
     1.3 @@ -104,6 +104,7 @@
     1.4    fun get_thes thy = Data.get thy
     1.5    fun add_thes thes thy = let
     1.6      fun add_the (the, theID) = insrt theID the theID
     1.7 +    (*needs no (!check_guhs_unique) because guh is generated automatically*)
     1.8    in Data.map (fold add_the thes) thy end;
     1.9  end;
    1.10  *}
    1.11 @@ -148,7 +149,6 @@
    1.12        ML_Context.the_generic_context () |> Context.theory_of |> KEStore_Elems.get_mets;
    1.13  fun get_thes () = 
    1.14        ML_Context.the_generic_context () |> Context.theory_of |> KEStore_Elems.get_thes;
    1.15 -(*fun get_thes () = ! thehier; SWITCH*)
    1.16  *}
    1.17  setup {* KEStore_Elems.add_rlss 
    1.18    [("e_rls", (Context.theory_name @{theory}, e_rls)), 
    1.19 @@ -165,10 +165,6 @@
    1.20  val (theID3, thydata3) = 
    1.21    (["IsacScripts"] : theID, Html {guh = part2guh ["IsacScripts"], html = "",
    1.22      mathauthors = ["Isac team"], coursedesign = []})
    1.23 -;
    1.24 -thehier := insrt theID1 thydata1 theID1 (get_thes ());
    1.25 -thehier := insrt theID2 thydata2 theID2 (get_thes ());
    1.26 -thehier := insrt theID3 thydata3 theID3 (get_thes ());
    1.27  *}
    1.28  setup {* (* determine sequence of main parts in thehier *)
    1.29  KEStore_Elems.add_thes

     2.1 --- a/src/Tools/isac/Knowledge/Biegelinie.thy	Thu Jun 05 15:49:44 2014 +0200
     2.2 +++ b/src/Tools/isac/Knowledge/Biegelinie.thy	Thu Jun 05 16:41:42 2014 +0200
     2.3 @@ -70,31 +70,6 @@
     2.4    (*according to rls 'simplify_Integral': .. = 1/a * .. instead .. = ../ a*)
     2.5    make_fun_explicit:     "Not (a =!= 0) ==> (a * (f x) = b) = (f x = 1/a * b)"
     2.6  
     2.7 -ML {*
     2.8 -val thy = @{theory};
     2.9 -
    2.10 -(** theory elements for transfer into html **)
    2.11 -store_thes 
    2.12 -  [make_thy @{theory}
    2.13 -    ["Walther Neuper 2005 supported by a grant from NMI Austria"],
    2.14 -  make_isa @{theory} ("IsacKnowledge", "Theorems")
    2.15 -    ["Walther Neuper 2005 supported by a grant from NMI Austria"],
    2.16 -  make_thm thy "IsacKnowledge" ("Belastung_Querkraft", prop_of @{thm Belastung_Querkraft})
    2.17 -	  ["Walther Neuper 2005 supported by a grant from NMI Austria"],
    2.18 -  make_thm thy "IsacKnowledge" ("Moment_Neigung", prop_of @{thm Moment_Neigung})
    2.19 -	  ["Walther Neuper 2005 supported by a grant from NMI Austria"],
    2.20 -  make_thm thy "IsacKnowledge" ("Moment_Querkraft", prop_of @{thm Moment_Querkraft})
    2.21 -	  ["Walther Neuper 2005 supported by a grant from NMI Austria"],
    2.22 -  make_thm thy "IsacKnowledge" ("Neigung_Moment", prop_of @{thm Neigung_Moment})
    2.23 -	  ["Walther Neuper 2005 supported by a grant from NMI Austria"],
    2.24 -  make_thm thy "IsacKnowledge" ("Querkraft_Belastung", prop_of @{thm Querkraft_Belastung})
    2.25 -	  ["Walther Neuper 2005 supported by a grant from NMI Austria"],
    2.26 -  make_thm thy "IsacKnowledge" ("Querkraft_Moment", prop_of @{thm Querkraft_Moment})
    2.27 -	  ["Walther Neuper 2005 supported by a grant from NMI Austria"],
    2.28 -  make_thm thy "IsacKnowledge" ("make_fun_explicit", prop_of @{thm make_fun_explicit})
    2.29 -	  ["Walther Neuper 2005 supported by a grant from NMI Austria"]
    2.30 -  ]
    2.31 -*}
    2.32  setup {*
    2.33  KEStore_Elems.add_thes
    2.34    [make_thy @{theory}
    2.35 @@ -119,14 +94,14 @@
    2.36  
    2.37  (** problems **)
    2.38  setup {* KEStore_Elems.add_pbts
    2.39 -  [(prep_pbt thy "pbl_bieg" [] e_pblID
    2.40 +  [(prep_pbt @{theory} "pbl_bieg" [] e_pblID
    2.41        (["Biegelinien"],
    2.42          [("#Given" ,["Traegerlaenge l_l", "Streckenlast q_q"]),
    2.43            (*("#Where",["0 < l_l"]), ...wait for &lt; and handling Arbfix*)
    2.44            ("#Find"  ,["Biegelinie b_b"]),
    2.45            ("#Relate",["Randbedingungen r_b"])],
    2.46          append_rls "e_rls" e_rls [], NONE, [["IntegrierenUndKonstanteBestimmen2"]])),
    2.47 -    (prep_pbt thy "pbl_bieg_mom" [] e_pblID
    2.48 +    (prep_pbt @{theory} "pbl_bieg_mom" [] e_pblID
    2.49        (["MomentBestimmte","Biegelinien"],
    2.50          [("#Given" ,["Traegerlaenge l_l", "Streckenlast q_q"]),
    2.51            (*("#Where",["0 < l_l"]), ...wait for &lt; and handling Arbfix*)
    2.52 @@ -134,26 +109,26 @@
    2.53            ("#Relate",["RandbedingungenBiegung r_b","RandbedingungenMoment r_m"])
    2.54          ],
    2.55          append_rls "e_rls" e_rls [], NONE, [["IntegrierenUndKonstanteBestimmen"]])),
    2.56 -    (prep_pbt thy "pbl_bieg_momg" [] e_pblID
    2.57 +    (prep_pbt @{theory} "pbl_bieg_momg" [] e_pblID
    2.58        (["MomentGegebene","Biegelinien"], [], append_rls "e_rls" e_rls [], NONE,
    2.59          [["IntegrierenUndKonstanteBestimmen","2xIntegrieren"]])),
    2.60 -    (prep_pbt thy "pbl_bieg_einf" [] e_pblID
    2.61 +    (prep_pbt @{theory} "pbl_bieg_einf" [] e_pblID
    2.62        (["einfache","Biegelinien"], [], append_rls "e_rls" e_rls [], NONE,
    2.63          [["IntegrierenUndKonstanteBestimmen","4x4System"]])),
    2.64 -    (prep_pbt thy "pbl_bieg_momquer" [] e_pblID
    2.65 +    (prep_pbt @{theory} "pbl_bieg_momquer" [] e_pblID
    2.66        (["QuerkraftUndMomentBestimmte","Biegelinien"], [], append_rls "e_rls" e_rls [], NONE,
    2.67          [["IntegrierenUndKonstanteBestimmen","1xIntegrieren"]])),
    2.68 -    (prep_pbt thy "pbl_bieg_vonq" [] e_pblID
    2.69 +    (prep_pbt @{theory} "pbl_bieg_vonq" [] e_pblID
    2.70        (["vonBelastungZu","Biegelinien"],
    2.71            [("#Given" ,["Streckenlast q_q","FunktionsVariable v_v"]),
    2.72              ("#Find"  ,["Funktionen funs'''"])],
    2.73          append_rls "e_rls" e_rls [], NONE, [["Biegelinien","ausBelastung"]])),
    2.74 -    (prep_pbt thy "pbl_bieg_randbed" [] e_pblID
    2.75 +    (prep_pbt @{theory} "pbl_bieg_randbed" [] e_pblID
    2.76        (["setzeRandbedingungen","Biegelinien"],
    2.77            [("#Given" ,["Funktionen fun_s","Randbedingungen r_b"]),
    2.78              ("#Find"  ,["Gleichungen equs'''"])],
    2.79          append_rls "e_rls" e_rls [], NONE, [["Biegelinien","setzeRandbedingungenEin"]])),
    2.80 -    (prep_pbt thy "pbl_equ_fromfun" [] e_pblID
    2.81 +    (prep_pbt @{theory} "pbl_equ_fromfun" [] e_pblID
    2.82        (["makeFunctionTo","equation"],
    2.83            [("#Given" ,["functionEq fu_n","substitution su_b"]),
    2.84              ("#Find"  ,["equality equ'''"])],
    2.85 @@ -210,7 +185,7 @@
    2.86  *}
    2.87  
    2.88  setup {* KEStore_Elems.add_mets
    2.89 -  [prep_met thy "met_biege" [] e_metID 
    2.90 +  [prep_met @{theory} "met_biege" [] e_metID 
    2.91  	    (["IntegrierenUndKonstanteBestimmen"],
    2.92  	      [("#Given" ,["Traegerlaenge l_l", "Streckenlast q__q", "FunktionsVariable v_v"]),
    2.93  		      (*("#Where",["0 < l_l"]), ...wait for &lt; and handling Arbfix*)
    2.94 @@ -286,7 +261,7 @@
    2.95            "       B__B = ((Substitute c_1_2) @@                                    " ^
    2.96            "              (Rewrite_Set_Inst [(bdv, x)] make_ratpoly_in False)) B__B " ^
    2.97            " in B__B)"),
    2.98 -    prep_met thy "met_biege_2" [] e_metID
    2.99 +    prep_met @{theory} "met_biege_2" [] e_metID
   2.100  	    (["IntegrierenUndKonstanteBestimmen2"],
   2.101  	      [("#Given" ,["Traegerlaenge l_l", "Streckenlast q__q", "FunktionsVariable v_v"]),
   2.102  		      (*("#Where",["0 < l_l"]), ...wait for &lt; and handling Arbfix*)
   2.103 @@ -323,27 +298,27 @@
   2.104            "       B_B = ((Substitute con_s) @@                                       " ^
   2.105            "              (Rewrite_Set_Inst [(bdv, v_v)] make_ratpoly_in False)) B_B  " ^
   2.106            " in B_B)"),
   2.107 -    prep_met thy "met_biege_intconst_2" [] e_metID
   2.108 +    prep_met @{theory} "met_biege_intconst_2" [] e_metID
   2.109  	    (["IntegrierenUndKonstanteBestimmen","2xIntegrieren"], [],
   2.110  	      {rew_ord'="tless_true", rls'=Erls, calc = [], srls = e_rls, prls=e_rls, crls = Atools_erls,
   2.111            errpats = [], nrls = e_rls},
   2.112          "empty_script"),
   2.113 -    prep_met thy "met_biege_intconst_4" [] e_metID
   2.114 +    prep_met @{theory} "met_biege_intconst_4" [] e_metID
   2.115  	    (["IntegrierenUndKonstanteBestimmen","4x4System"], [],
   2.116  	      {rew_ord'="tless_true", rls'=Erls, calc = [], srls = e_rls, prls=e_rls, crls = Atools_erls,
   2.117            errpats = [], nrls = e_rls},
   2.118          "empty_script"),
   2.119 -    prep_met thy "met_biege_intconst_1" [] e_metID
   2.120 +    prep_met @{theory} "met_biege_intconst_1" [] e_metID
   2.121  	    (["IntegrierenUndKonstanteBestimmen","1xIntegrieren"], [],
   2.122          {rew_ord'="tless_true", rls'=Erls, calc = [], srls = e_rls, prls=e_rls, crls = Atools_erls,
   2.123            errpats = [], nrls = e_rls},
   2.124          "empty_script"),
   2.125 -    prep_met thy "met_biege2" [] e_metID
   2.126 +    prep_met @{theory} "met_biege2" [] e_metID
   2.127  	    (["Biegelinien"], [],
   2.128  	      {rew_ord'="tless_true", rls'=Erls, calc = [], srls = e_rls, prls=e_rls, crls = Atools_erls,
   2.129            errpats = [], nrls = e_rls},
   2.130          "empty_script"),
   2.131 -    prep_met thy "met_biege_ausbelast" [] e_metID
   2.132 +    prep_met @{theory} "met_biege_ausbelast" [] e_metID
   2.133  	    (["Biegelinien", "ausBelastung"],
   2.134  	      [("#Given" ,["Streckenlast q__q", "FunktionsVariable v_v"]),
   2.135  	        ("#Find"  ,["Funktionen fun_s"])],
   2.136 @@ -380,7 +355,7 @@
   2.137            "                          [diff,integration,named])                    " ^
   2.138            "                          [REAL (rhs N__N), REAL v_v, REAL_REAL y])    " ^
   2.139            " in [Q__Q, M__M, N__N, B__B])"),
   2.140 -    prep_met thy "met_biege_setzrand" [] e_metID
   2.141 +    prep_met @{theory} "met_biege_setzrand" [] e_metID
   2.142  	    (["Biegelinien", "setzeRandbedingungenEin"],
   2.143  	      [("#Given" , ["Funktionen fun_s", "Randbedingungen r_b"]),
   2.144  	        ("#Find"  , ["Gleichungen equs'''"])],
   2.145 @@ -439,7 +414,7 @@
   2.146            "                          [Equation,fromFunction])              " ^
   2.147            "                          [BOOL (hd f_s), BOOL b_4])          " ^
   2.148            " in [e_1,e_2,e_3,e_4])"*)),
   2.149 -    prep_met thy "met_equ_fromfun" [] e_metID
   2.150 +    prep_met @{theory} "met_equ_fromfun" [] e_metID
   2.151  	    (["Equation","fromFunction"],
   2.152  	      [("#Given" ,["functionEq fu_n","substitution su_b"]),
   2.153  	        ("#Find"  ,["equality equ'''"])],

     3.1 --- a/src/Tools/isac/Knowledge/Build_Thydata.thy	Thu Jun 05 15:49:44 2014 +0200
     3.2 +++ b/src/Tools/isac/Knowledge/Build_Thydata.thy	Thu Jun 05 16:41:42 2014 +0200
     3.3 @@ -90,8 +90,8 @@
     3.4    collect_part       "IsacScripts" proglang_parent progthys'
     3.5  : (theID * thydata) list
     3.6  ;
     3.7 -thehier := the_hier (get_thes ()) thydata_list;
     3.8 -(*tracing("----------------------------------\n" ^
     3.9 +(*thehier := the_hier (get_thes ()) thydata_list;
    3.10 +tracing("----------------------------------\n" ^
    3.11  	"*** insert: not found ... IS OK : \n" ^
    3.12  	"comes from fill_parents           \n" ^
    3.13  	"----------------------------------\n");*)
    3.14 @@ -99,32 +99,7 @@
    3.15  
    3.16  section {* interface for dialog-authoring *}
    3.17  
    3.18 -ML {*
    3.19  (*/========= inhibit exn WN130620 (1.4.1) below: fill thehier ==============\*)
    3.20 -store_thes 
    3.21 -  [make_thy @{theory "Diff"} ["Isabelle2011-->12"],
    3.22 -  make_isa @{theory "Diff"} ("IsacKnowledge", "Theorems") ["Isabelle2011-->12"],
    3.23 -  make_thm @{theory "Diff"} "IsacKnowledge" ("diff_sin_chain", prop_of @{thm diff_sin_chain})
    3.24 -   ["Isabelle2011-->12"],
    3.25 -  make_thm @{theory "Diff"} "IsacKnowledge" ("diff_cos_chain", prop_of @{thm diff_cos_chain})
    3.26 -   ["Isabelle2011-->12"],
    3.27 -  make_thm @{theory "Diff"} "IsacKnowledge" ("diff_pow_chain", prop_of @{thm diff_pow_chain})
    3.28 -   ["Isabelle2011-->12"],
    3.29 -  make_thm @{theory "Diff"} "IsacKnowledge" ("diff_ln_chain", prop_of @{thm diff_ln_chain})
    3.30 -   ["Isabelle2011-->12"],
    3.31 -  make_thm @{theory "Diff"} "IsacKnowledge" ("diff_exp_chain", prop_of @{thm diff_exp_chain})
    3.32 -   ["Isabelle2011-->12"],
    3.33 -
    3.34 -  make_isa @{theory "Diff"} ("IsacKnowledge", "Rulesets") ["Isabelle2011-->12"],
    3.35 -  make_rls @{theory "Diff"} norm_diff ["Isabelle2011-->12"],
    3.36 -
    3.37 -  make_thy @{theory "Test"} ["Isabelle2011-->12"],
    3.38 -  make_isa @{theory "Test"} ("IsacKnowledge", "Theorems") ["Isabelle2011-->12"],
    3.39 -  make_thm @{theory "Test"} "IsacKnowledge" ("radd_left_commute", prop_of @{thm radd_left_commute})
    3.40 -   ["Isabelle2011-->12"]
    3.41 -  ]
    3.42 -(*\========= inhibit exn WN130620 (1.4.1) below: fill thehier ==============/*)
    3.43 -*}
    3.44  setup {*
    3.45  KEStore_Elems.add_thes
    3.46    [make_thy @{theory "Diff"} ["Isabelle2011-->12"],
    3.47 @@ -148,6 +123,7 @@
    3.48    make_thm @{theory "Test"} "IsacKnowledge" ("radd_left_commute", prop_of @{thm radd_left_commute})
    3.49     ["Isabelle2011-->12"]]
    3.50  *}
    3.51 +(*\========= inhibit exn WN130620 (1.4.1) below: fill thehier ==============/*)
    3.52  
    3.53  subsection {* Add error patterns *}
    3.54  subsubsection {* Error patterns for differentiation *}
    3.55 @@ -164,21 +140,6 @@
    3.56            @{thm  diff_exp_chain}])]]
    3.57  *}
    3.58  
    3.59 -ML {*
    3.60 -store_thes 
    3.61 -  [insert_fillpats ["IsacKnowledge", "Diff", "Theorems", "diff_sin_chain"]
    3.62 - ([("fill-d_d-arg",
    3.63 -     parse_patt @{theory Diff} "d_d ?bdv (sin ?u) = cos ?u * d_d ?bdv _", "chain-rule-diff-both"),
    3.64 -   ("fill-both-args",
    3.65 -     parse_patt @{theory Diff} "d_d ?bdv (sin _) = cos ?u * d_d ?bdv _", "chain-rule-diff-both"),
    3.66 -   ("fill-d_d",
    3.67 -     parse_patt @{theory Diff} "d_d ?bdv (sin ?u) = cos ?u * _ ?bdv ?u", "chain-rule-diff-both"),
    3.68 -   ("fill-inner-deriv",
    3.69 -     parse_patt @{theory Diff} "d_d ?bdv (sin ?u) = cos ?u * _", "chain-rule-diff-both"),
    3.70 -   ("fill-all",
    3.71 -     parse_patt @{theory Diff} "d_d ?bdv (sin ?u) = _", "chain-rule-diff-both")]: fillpat list)
    3.72 -  ]
    3.73 -*}
    3.74  setup {*
    3.75  KEStore_Elems.add_thes
    3.76    [insert_fillpats ["IsacKnowledge", "Diff", "Theorems", "diff_sin_chain"]

     4.1 --- a/src/Tools/isac/calcelems.sml	Thu Jun 05 15:49:44 2014 +0200
     4.2 +++ b/src/Tools/isac/calcelems.sml	Thu Jun 05 16:41:42 2014 +0200
     4.3 @@ -484,7 +484,6 @@
     4.4  val e_thydata = Html {guh="e_guh", coursedesign=[], mathauthors=[], html=""};
     4.5  
     4.6  type thehier = (thydata ptyp) list;
     4.7 -val thehier = Unsynchronized.ref ([] : thehier); (*WN101011 make argument, del*)
     4.8  (* required to determine sequence of main nodes of thehier in KEStore.thy *)
     4.9  fun part2guh ([str]:theID) =
    4.10      (case str of
    4.11 @@ -903,7 +902,7 @@
    4.12  
    4.13  fun coll_metguhs mets =
    4.14      let fun node coll (Ptyp (_,[n],ns)) =
    4.15 -	    [(#guh : met -> guh) n]
    4.16 +	    [(#guh : met -> guh) n] @ (nodes coll ns)
    4.17  	and nodes coll [] = coll
    4.18  	  | nodes coll (n::ns) = (node coll n) @ (nodes coll ns);
    4.19      in nodes [] mets end;

     5.1 --- a/src/Tools/isac/xmlsrc/thy-hierarchy.sml	Thu Jun 05 15:49:44 2014 +0200
     5.2 +++ b/src/Tools/isac/xmlsrc/thy-hierarchy.sml	Thu Jun 05 16:41:42 2014 +0200
     5.3 @@ -367,12 +367,6 @@
     5.4  			ord = ord}
     5.5    in (the, theID) end
     5.6  
     5.7 -(*needs no (!check_guhs_unique) because guh is generated automatically*)
     5.8 -fun store_thes thes thy = 
     5.9 -  let 
    5.10 -    fun store_the (the, theID) thy = thehier := insrt theID the theID (get_thes ())
    5.11 -  in fold store_the thes () end
    5.12 -
    5.13  fun update_hthm (Hthm {guh, coursedesign, mathauthors, thm, ...}) fillpats' =
    5.14    Hthm {guh = guh, coursedesign = coursedesign, mathauthors = mathauthors,
    5.15      fillpats = fillpats', thm = thm}

     6.1 --- a/test/Tools/isac/Knowledge/build_thydata.sml	Thu Jun 05 15:49:44 2014 +0200
     6.2 +++ b/test/Tools/isac/Knowledge/build_thydata.sml	Thu Jun 05 16:41:42 2014 +0200
     6.3 @@ -337,7 +337,8 @@
     6.4  "-------- the_hier (get_thes ()) thydata_list -------------";
     6.5  "-------- the_hier (get_thes ()) thydata_list -------------";
     6.6  "-------- the_hier (get_thes ()) thydata_list -------------";
     6.7 -thehier; (* = ref [Ptyp ("IsacKnowledge", [Html {guh = "thy_isac_IsacKnowledge-part", ...}],
     6.8 +(*KEStore_Elems.get_thes (Thy_Info.get_theory "Build_Thydata"); ...this overstrains Output buffer*) 
     6.9 + (* = ref [Ptyp ("IsacKnowledge", [Html {guh = "thy_isac_IsacKnowledge-part", ...}],
    6.10                      [Ptyp ("Biegelinie", [Html {guh = "thy_isac_Biegelinie", ...}],
    6.11                        [Ptyp ("Theorems", [Html {guh = "thy_isac_Biegelinie-Theorems", ...}],
    6.12                          [Ptyp ("Belastung_Querkraft", [Hthm {guh = "thy_isac_B ...}],[]),

     7.1 --- a/test/Tools/isac/Knowledge/isac.sml	Thu Jun 05 15:49:44 2014 +0200
     7.2 +++ b/test/Tools/isac/Knowledge/isac.sml	Thu Jun 05 16:41:42 2014 +0200
     7.3 @@ -8,8 +8,6 @@
     7.4      val allthys = @{theory} :: Theory.ancestors_of @{theory};
     7.5  
     7.6  @{theory} is NOT Isac.thy, but some predecessor, which causes 
     7.7 -the error 'ME_Isac "Isac" not in system' in
     7.8 -
     7.9 -    thehier := the_hier (get_thes ()) (collect_thydata ());
    7.10 +the error 'ME_Isac "Isac" not in system'.
    7.11  *)
    7.12  

     8.1 --- a/test/Tools/isac/xmlsrc/thy-hierarchy.sml	Thu Jun 05 15:49:44 2014 +0200
     8.2 +++ b/test/Tools/isac/xmlsrc/thy-hierarchy.sml	Thu Jun 05 16:41:42 2014 +0200
     8.3 @@ -113,7 +113,7 @@
     8.4  "----------- the_hier [] (collect_thyda.. NOT overwriting store_ -";
     8.5  "----------- the_hier [] (collect_thyda.. NOT overwriting store_ -";
     8.6  "----------- the_hier [] (collect_thyda.. NOT overwriting store_ -";
     8.7 -(* with "setup KEStore" this cannot be done
     8.8 +(* with "setup KEStore" this cannot be done ...
     8.9  store_isa ["Isabelle"] ["THIS SHOULD not BE OVERWRITTEN below"];
    8.10  print_depth 99; get_the ["Isabelle"]; print_depth 3;
    8.11  print_depth 5; thehier;  print_depth 3;
    8.12 @@ -300,7 +300,7 @@
    8.13  if errpattIDs = ["chain-rule-diff-both", "test-errpatID"] then ()
    8.14  else error "insert_errpatIDs to norm_diff changed";
    8.15  
    8.16 -(* isolate test: 10 secs *) thehier := original;
    8.17 +(* isolate test: 10 secs  thehier := original; *)
    8.18  ^^^^^--- this intermediate save/restore does not work and affects other tests ---^^*)
    8.19  
    8.20  insert_fillpats ["IsacKnowledge", "Diff", "Theorems", "diff_sin_chain"]