1.1 --- a/src/Tools/isac/calcelems.sml	Sat Jan 20 13:00:40 2018 +0100
     1.2 +++ b/src/Tools/isac/calcelems.sml	Sat Jan 20 13:19:01 2018 +0100
     1.3 @@ -828,7 +828,7 @@
     1.4    | scr2str (Rfuns _)  = "Rfuns";
     1.5  
     1.6  
     1.7 -fun maxthy thy1 thy2 = if Theory.subthy (thy1, thy2) then thy2 else thy1;
     1.8 +fun maxthy thy1 thy2 = if Context.subthy (thy1, thy2) then thy2 else thy1;
     1.9  
    1.10  
    1.11  (*.trace internal steps of isac's rewriter*)
    1.12 @@ -1090,47 +1090,47 @@
    1.13    let
    1.14      val allthys = Theory.ancestors_of (Thy_Info.get_theory "Build_Thydata")
    1.15    in
    1.16 -    drop ((find_index (curry Theory.eq_thy (Thy_Info.get_theory "Complex_Main")) allthys), allthys)
    1.17 +    drop ((find_index (curry Context.eq_thy (Thy_Info.get_theory "Complex_Main")) allthys), allthys)
    1.18    end
    1.19  fun knowthys () = (*["Isac", .., "Descript", "Delete"]*)
    1.20    let
    1.21      fun isacthys () = (* ["Isac", .., "KEStore"] without Build_Isac thys: "Interpret" etc *)
    1.22        let
    1.23 -        val allthys = filter_out (member Theory.eq_thy
    1.24 +        val allthys = filter_out (member Context.eq_thy
    1.25            [(*Thy_Info.get_theory "ProgLang",*) Thy_Info.get_theory "Interpret", 
    1.26              Thy_Info.get_theory "xmlsrc", Thy_Info.get_theory "Frontend"]) 
    1.27            (Theory.ancestors_of (Thy_Info.get_theory "Build_Thydata"))
    1.28        in
    1.29 -        take ((find_index (curry Theory.eq_thy (Thy_Info.get_theory "Complex_Main")) allthys), 
    1.30 +        take ((find_index (curry Context.eq_thy (Thy_Info.get_theory "Complex_Main")) allthys), 
    1.31          allthys)
    1.32        end
    1.33      val isacthys' = isacthys ()
    1.34      val proglang_parent = Thy_Info.get_theory "ProgLang"
    1.35    in
    1.36 -    take ((find_index (curry Theory.eq_thy proglang_parent) isacthys'), isacthys')
    1.37 +    take ((find_index (curry Context.eq_thy proglang_parent) isacthys'), isacthys')
    1.38    end
    1.39  fun progthys () = (*["Isac", .., "Descript", "Delete"]*)
    1.40    let
    1.41      fun isacthys () = (* ["Isac", .., "KEStore"] without Build_Isac thys: "Interpret" etc *)
    1.42        let
    1.43 -        val allthys = filter_out (member Theory.eq_thy
    1.44 +        val allthys = filter_out (member Context.eq_thy
    1.45            [(*Thy_Info.get_theory "ProgLang",*) Thy_Info.get_theory "Interpret", 
    1.46              Thy_Info.get_theory "xmlsrc", Thy_Info.get_theory "Frontend"]) 
    1.47            (Theory.ancestors_of (Thy_Info.get_theory "Build_Thydata"))
    1.48        in
    1.49 -        take ((find_index (curry Theory.eq_thy (Thy_Info.get_theory "Complex_Main")) allthys), 
    1.50 +        take ((find_index (curry Context.eq_thy (Thy_Info.get_theory "Complex_Main")) allthys), 
    1.51          allthys)
    1.52        end
    1.53      val isacthys' = isacthys ()
    1.54      val proglang_parent = Thy_Info.get_theory "ProgLang"
    1.55    in
    1.56 -    drop ((find_index (curry Theory.eq_thy proglang_parent) isacthys') + 1(*ProgLang*), isacthys')
    1.57 +    drop ((find_index (curry Context.eq_thy proglang_parent) isacthys') + 1(*ProgLang*), isacthys')
    1.58    end
    1.59  
    1.60  fun partID thy = 
    1.61 -  if member Theory.eq_thy (knowthys ()) thy then "IsacKnowledge"
    1.62 -  else if member Theory.eq_thy (progthys ()) thy then "IsacScripts"
    1.63 -  else if member Theory.eq_thy (isabthys ()) thy then "Isabelle"
    1.64 +  if member Context.eq_thy (knowthys ()) thy then "IsacKnowledge"
    1.65 +  else if member Context.eq_thy (progthys ()) thy then "IsacScripts"
    1.66 +  else if member Context.eq_thy (isabthys ()) thy then "Isabelle"
    1.67    else error ("closure of thys in Isac is broken by " ^ string_of_thy thy)
    1.68  fun partID' (thy' : theory') = partID (Thy_Info.get_theory thy')
    1.69  (*