1.1 --- a/src/Tools/isac/Interpret/ctree-basic.sml	Thu Mar 08 07:52:06 2018 +0100
     1.2 +++ b/src/Tools/isac/Interpret/ctree-basic.sml	Thu Mar 08 08:04:04 2018 +0100
     1.3 @@ -205,7 +205,7 @@
     1.4  val e_pos' = ([], Und);
     1.5  
     1.6  (* ATTENTION: does _not_ recognise Variable.declare_constraints, etc...*)
     1.7 -fun is_e_ctxt ctxt = Context.eq_thy (Proof_Context.theory_of ctxt, @{theory "Isac"});
     1.8 +fun is_e_ctxt ctxt = Context.eq_thy (Proof_Context.theory_of ctxt, @{theory "Pure"});
     1.9  
    1.10  type iist = Selem.istate option * Selem.istate option;
    1.11  (*val e_iist = (e_istate, e_istate); --- sinnlos f"ur NICHT-equality-type*) 

     2.1 --- a/src/Tools/isac/Interpret/specification-elems.sml	Thu Mar 08 07:52:06 2018 +0100
     2.2 +++ b/src/Tools/isac/Interpret/specification-elems.sml	Thu Mar 08 08:04:04 2018 +0100
     2.3 @@ -126,6 +126,6 @@
     2.4  fun sube2subst thy s = map (TermC.dest_equals o (TermC.parse_patt thy)) s;
     2.5  val sube2subte = map TermC.str2term;
     2.6  val subte2subst = map HOLogic.dest_eq;
     2.7 -val e_ctxt = Proof_Context.init_global @{theory "Isac"};
     2.8 +val e_ctxt = Proof_Context.init_global @{theory "Pure"};
     2.9  
    2.10  end

     3.1 --- a/src/Tools/isac/Knowledge/Root.thy	Thu Mar 08 07:52:06 2018 +0100
     3.2 +++ b/src/Tools/isac/Knowledge/Root.thy	Thu Mar 08 08:04:04 2018 +0100
     3.3 @@ -157,7 +157,7 @@
     3.4  
     3.5  rew_ord' := overwritel (!rew_ord',
     3.6  [("termlessI", termlessI),
     3.7 - ("sqrt_right", sqrt_right false @{theory "Isac"})
     3.8 + ("sqrt_right", sqrt_right false @{theory "Pure"})
     3.9   ]);
    3.10  
    3.11  (*-------------------------rulse-------------------------*)

     4.1 --- a/src/Tools/isac/Knowledge/Test.thy	Thu Mar 08 07:52:06 2018 +0100
     4.2 +++ b/src/Tools/isac/Knowledge/Test.thy	Thu Mar 08 08:04:04 2018 +0100
     4.3 @@ -248,7 +248,7 @@
     4.4  (*FIXXXXXXME 10.8.02: handle like _simplify*)
     4.5  val tval_rls =  
     4.6    Rls{id = "tval_rls", preconds = [], 
     4.7 -      rew_ord = ("sqrt_right",sqrt_right false @{theory "Isac"}), 
     4.8 +      rew_ord = ("sqrt_right",sqrt_right false @{theory "Pure"}), 
     4.9        erls=testerls,srls = e_rls, 
    4.10        calc=[], errpatts = [],
    4.11        rules = [Thm ("refl",TermC.num_str @{thm refl}),
    4.12 @@ -379,7 +379,7 @@
    4.13  (* expects * distributed over + *)
    4.14  val Test_simplify =
    4.15    Rls{id = "Test_simplify", preconds = [], 
    4.16 -      rew_ord = ("sqrt_right",sqrt_right false @{theory "Isac"}),
    4.17 +      rew_ord = ("sqrt_right",sqrt_right false @{theory "Pure"}),
    4.18        erls = tval_rls, srls = e_rls, 
    4.19        calc=[(*since 040209 filled by prep_rls'*)], errpatts = [],
    4.20        rules = [

     5.1 --- a/src/Tools/isac/calcelems.sml	Thu Mar 08 07:52:06 2018 +0100
     5.2 +++ b/src/Tools/isac/calcelems.sml	Thu Mar 08 08:04:04 2018 +0100
     5.3 @@ -905,7 +905,7 @@
     5.4                         for constraints on identifiers see "fun cpy_nam" *)
     5.5    met : metID list}   (* methods solving the pbt*)
     5.6  
     5.7 -val e_pbt = {guh = "pbl_empty", mathauthors = [], init = e_pblID, thy = Thy_Info.get_theory "Isac",
     5.8 +val e_pbt = {guh = "pbl_empty", mathauthors = [], init = e_pblID, thy = Thy_Info.get_theory "Pure",
     5.9    cas = NONE, prls = Erls, where_ = [], ppc = [], met = []} : pbt
    5.10  fun pbt2str
    5.11          ({cas = cas', guh = guh', init = init', mathauthors = ma', met = met', ppc = ppc',
    5.12 @@ -1102,7 +1102,7 @@
    5.13  
    5.14  (* group the theories defined in Isac, compare Build_Thydata:
    5.15    section "Get and group the theories defined in Isac" *) 
    5.16 -fun isabthys () = (*["Complex_Main", "Taylor", .., "Isac"]*)
    5.17 +fun isabthys () = (*["Complex_Main", "Taylor", .., "Pure"]*)
    5.18    let
    5.19      val allthys = Theory.ancestors_of (Thy_Info_get_theory "Build_Thydata")
    5.20    in