1.1 --- a/test/Tools/isac/BridgeLibisabelle/datatypes.sml	Tue Apr 21 12:26:08 2020 +0200
     1.2 +++ b/test/Tools/isac/BridgeLibisabelle/datatypes.sml	Tue Apr 21 15:42:50 2020 +0200
     1.3 @@ -85,7 +85,7 @@
     1.4  Iterator 1;
     1.5  moveActiveRoot 1; autoCalculate 1 CompleteCalc;
     1.6  refineProblem 1 ([1],Res) "pbl_equ_univ"; 
     1.7 -"~~~~~ fun refineProblem, args:"; val (cI, ((p,p_) : pos'), (guh : guh)) = 
     1.8 +"~~~~~ fun refineProblem, args:"; val (cI, ((p,p_) : pos'), (guh : Check_Unique.guh)) = 
     1.9    (1, ([1],Res), "pbl_equ_univ");
    1.10  val pblID = guh2kestoreID guh
    1.11  	 val ((pt,_),_) = get_calc cI
    1.12 @@ -264,14 +264,14 @@
    1.13  Model_Problem: Tactic.input;
    1.14  Or_to_List: Tactic.input;
    1.15  
    1.16 -Apply_Method: metID -> Tactic.input;
    1.17 -Refine_Tacitly: pblID -> Tactic.input;
    1.18 -Specify_Problem: pblID -> Tactic.input;
    1.19 -Specify_Method: metID -> Tactic.input;
    1.20 +Apply_Method: Spec.metID -> Tactic.input;
    1.21 +Refine_Tacitly: Spec.pblID -> Tactic.input;
    1.22 +Specify_Problem: Spec.pblID -> Tactic.input;
    1.23 +Specify_Method: Spec.metID -> Tactic.input;
    1.24  Substitute: sube -> Tactic.input;; (* Substitute: sube -> tac; e_sube: TermC.as_string list; UNCLEAR HOW TO INPUT *)
    1.25 -Check_Postcond: pblID -> Tactic.input;
    1.26 +Check_Postcond: Spec.pblID -> Tactic.input;
    1.27  
    1.28 -Apply_Method: metID -> Tactic.input;
    1.29 +Apply_Method: Spec.metID -> Tactic.input;
    1.30  val tac = Apply_Method(["test", "equation", "simplify"]);
    1.31  xml_of_tac tac;(*
    1.32  <STRINGLISTTACTIC name="Apply_Method">