src/Tools/isac/BridgeLibisabelle/interface.sml
changeset 59921 0766dade4a78
parent 59920 33913fe24685
child 59932 87336f3b021f
     1.1 --- a/src/Tools/isac/BridgeLibisabelle/interface.sml	Wed Apr 29 12:30:51 2020 +0200
     1.2 +++ b/src/Tools/isac/BridgeLibisabelle/interface.sml	Fri May 01 15:28:40 2020 +0200
     1.3 @@ -344,7 +344,7 @@
     1.4  		      | ("end-of-calculation", _) => message2xml cI "end-of-calculation"
     1.5  		      | ("failure", _) => sysERROR2xml cI "failure"
     1.6  		      | ("not-applicable", _) => (*the rule comes from anywhere..*)
     1.7 -		          (case ApplicableOLD.applicable_in ip pt tac of
     1.8 +		          (case Step.check tac (pt, ip) of
     1.9  		            Applicable.No e => message2xml cI ("'" ^ Tactic.input_to_string tac ^ "' not-applicable")
    1.10  	            | Applicable.Yes m =>
    1.11  		              let