src/Tools/isac/Interpret/solve.sml
changeset 59186 d9c3e373f8f5
parent 59121 37283f123688
child 59257 a1daf71787b1
     1.1 --- a/src/Tools/isac/Interpret/solve.sml	Mon Dec 07 10:52:07 2015 +0100
     1.2 +++ b/src/Tools/isac/Interpret/solve.sml	Mon Dec 07 11:25:02 2015 +0100
     1.3 @@ -117,8 +117,8 @@
     1.4  (* use"ME/solve.sml";
     1.5     use"solve.sml";
     1.6  
     1.7 -val ttt = (term_of o the o (parse thy))"Substitute [(bdv,x)] g";
     1.8 -val ttt = (term_of o the o (parse thy))"Rewrite thmid True g";
     1.9 +val ttt = (Thm.term_of o the o (parse thy))"Substitute [(bdv,x)] g";
    1.10 +val ttt = (Thm.term_of o the o (parse thy))"Rewrite thmid True g";
    1.11  
    1.12    Const ("Script.Rewrite'_Inst",_) $ sub $ Free (thm',_) $ Const (pa,_) $ f'
    1.13     *)