src/Tools/isac/Knowledge/Root.thy
changeset 59186 d9c3e373f8f5
parent 59107 a65b5af1475f
child 59360 729c3ca4e5fc
     1.1 --- a/src/Tools/isac/Knowledge/Root.thy	Mon Dec 07 10:52:07 2015 +0100
     1.2 +++ b/src/Tools/isac/Knowledge/Root.thy	Mon Dec 07 11:25:02 2015 +0100
     1.3 @@ -250,7 +250,7 @@
     1.4  	       Calc ("Groups.times_class.times", eval_binop "#mult_"),
     1.5  	       Calc ("Atools.pow", eval_binop "#power_")
     1.6  	       ],
     1.7 -      scr = Prog ((term_of o the o (parse thy)) "empty_script")
     1.8 +      scr = Prog ((Thm.term_of o the o (parse thy)) "empty_script")
     1.9        }:rls);      
    1.10  *}
    1.11  setup {* KEStore_Elems.add_rlss [("make_rooteq", (Context.theory_name @{theory}, make_rooteq))] *}
    1.12 @@ -324,7 +324,7 @@
    1.13  	       Calc ("NthRoot.sqrt",eval_sqrt "#sqrt_"),
    1.14  	       Calc ("Atools.pow", eval_binop "#power_")
    1.15  	       ],
    1.16 -      scr = Prog ((term_of o the o (parse thy)) "empty_script")
    1.17 +      scr = Prog ((Thm.term_of o the o (parse thy)) "empty_script")
    1.18         }:rls);      
    1.19  *}
    1.20  setup {* KEStore_Elems.add_rlss