src/Tools/isac/Knowledge/EqSystem.thy
changeset 59552 ab7955d2ead3
parent 59551 6ea6d9c377a0
child 59592 99c8d2ff63eb
     1.1 --- a/src/Tools/isac/Knowledge/EqSystem.thy	Sat Jun 22 14:34:06 2019 +0200
     1.2 +++ b/src/Tools/isac/Knowledge/EqSystem.thy	Sun Jun 23 14:23:09 2019 +0200
     1.3 @@ -208,7 +208,7 @@
     1.4  		(*Rule.Rls_ add_fractions_p, #2*)
     1.5  		Rule.Rls_ cancel_p
     1.6  		],
     1.7 -       scr = Rule.Prog ((Thm.term_of o the o (TermC.parse thy)) "empty_script")
     1.8 +       scr = Rule.EmptyScr
     1.9         };
    1.10  \<close>
    1.11  ML \<open>
    1.12 @@ -229,7 +229,7 @@
    1.13  		Rule.Rls_ add_fractions_p,
    1.14  		Rule.Rls_ cancel_p
    1.15  		],
    1.16 -       scr = Rule.Prog ((Thm.term_of o the o (TermC.parse thy)) "empty_script")
    1.17 +       scr = Rule.EmptyScr
    1.18         };
    1.19  \<close>
    1.20  ML \<open>