1.1 --- a/src/Tools/isac/Knowledge/Simplify.thy	Tue Feb 06 16:59:09 2018 +0100
     1.2 +++ b/src/Tools/isac/Knowledge/Simplify.thy	Wed Feb 07 10:24:16 2018 +0100
     1.3 @@ -58,7 +58,7 @@
     1.4  (*.function for handling the cas-input "Simplify (2*a + 3*a)":
     1.5     make a model which is already in ctree-internal format.*)
     1.6  (* val (h,argl) = strip_comb (str2term "Simplify (2*a + 3*a)");
     1.7 -   val (h,argl) = strip_comb ((Thm.term_of o the o (parse (Thy_Info.get_theory "Simplify"))) 
     1.8 +   val (h,argl) = strip_comb ((Thm.term_of o the o (parse (Thy_Info_get_theory "Simplify"))) 
     1.9  				  "Simplify (2*a + 3*a)");
    1.10     *)
    1.11  fun argl2dtss t =