src/Tools/isac/Interpret/script.sml
changeset 59272 1d3ef477d9c8
parent 59271 7a02202e4577
child 59276 56dc790071cb
     1.1 --- a/src/Tools/isac/Interpret/script.sml	Mon Dec 19 10:37:44 2016 +0100
     1.2 +++ b/src/Tools/isac/Interpret/script.sml	Wed Dec 21 08:57:47 2016 +0100
     1.3 @@ -675,7 +675,7 @@
     1.4               (case ap of   (*switch for Or: 1st AssOnly, 2nd AssGen*)
     1.5                  AssOnly => (NasNap (v, E))
     1.6                | _ =>
     1.7 -                  (case applicable_in (p,p_) pt (stac2tac pt (assoc_thy thy') stac) of
     1.8 +                  (case Applicable.applicable_in (p,p_) pt (stac2tac pt (assoc_thy thy') stac) of
     1.9  		                 Chead.Appl m' =>
    1.10  		                   let
    1.11                           val is = (E,l,a',tac_2res m',S,false(*FIXXXME.WN0?*))
    1.12 @@ -928,7 +928,7 @@
    1.13        in case m of 
    1.14  	      Subproblem _ => Appy (m', (E,l,a',tac_2res m',Sundef,false))
    1.15  	    | _ =>
    1.16 -        (case applicable_in p pt m of
    1.17 +        (case Applicable.applicable_in p pt m of
    1.18  		       Chead.Appl m' => (Appy (m', (E,l,a',tac_2res m',Sundef,false)))
    1.19  		     | _ => Napp E)
    1.20  	    end