1.1 --- a/test/Tools/isac/BridgeLibisabelle/datatypes.sml	Wed Apr 15 11:37:43 2020 +0200
     1.2 +++ b/test/Tools/isac/BridgeLibisabelle/datatypes.sml	Wed Apr 15 13:47:56 2020 +0200
     1.3 @@ -35,13 +35,13 @@
     1.4  (*val thydata = get_the ["IsacKnowledge", "Test", "Rulesets", "ac_plus_times"]; 
     1.5    (* ERROR: get_pbt not found: ["IsacKnowledge","Test","Rulesets","ac_plus_times"] *)*)
     1.6  "~~~~~ fun get_the, args:"; val (theID:theID) = (["IsacKnowledge", "Test", "Rulesets", "ac_plus_times"]);
     1.7 -(*get_py  (Thy_Info_get_theory "Pure") theID theID (get_thes ()); 
     1.8 +(*get_py  (ThyC.get_theory "Pure") theID theID (get_thes ()); 
     1.9    (* ERROR: get_pbt not found: ["IsacKnowledge","Test","Rulesets","ac_plus_times"] *)*)
    1.10  (*default_print_depth 3; 999*)
    1.11  (get_thes ());
    1.12  
    1.13 -(*"~~~~~ fun get_py, args:"; val (thy, d, _, []) = ((Thy_Info_get_theory "Pure"), theID, theID, (get_thes ()));*)
    1.14 -"~~~~~ fun get_py, args:"; val (thy, d, _, [_]) = ((Thy_Info_get_theory "Pure"), theID, theID, (get_thes ()));
    1.15 +(*"~~~~~ fun get_py, args:"; val (thy, d, _, []) = ((ThyC.get_theory "Pure"), theID, theID, (get_thes ()));*)
    1.16 +"~~~~~ fun get_py, args:"; val (thy, d, _, [_]) = ((ThyC.get_theory "Pure"), theID, theID, (get_thes ()));
    1.17  error ("get_pbt not found: "^(strs2str d));
    1.18  (*AK110725 To be continued...s*)
    1.19  *)
    1.20 @@ -247,7 +247,7 @@
    1.21  
    1.22  "----------- these are : string -> tac: ";
    1.23  Calculate: string -> Tactic.input;; (* should be the operator*)
    1.24 -Specify_Theory: domID -> Tactic.input;;
    1.25 +Specify_Theory: ThyC.id -> Tactic.input;;
    1.26  val tac = Specify_Theory("Differentiate");
    1.27  xml_of_tac tac;(*
    1.28  <SIMPLETACTIC name="Specify_Theory">