diff -r a474900d5bd2 -r 255c853ea2f0 src/Tools/isac/Knowledge/Simplify.thy --- a/src/Tools/isac/Knowledge/Simplify.thy Thu Dec 22 11:12:18 2016 +0100 +++ b/src/Tools/isac/Knowledge/Simplify.thy Thu Dec 22 11:36:20 2016 +0100 @@ -56,7 +56,7 @@ (** CAS-command **) (*.function for handling the cas-input "Simplify (2*a + 3*a)": - make a model which is already in ptree-internal format.*) + make a model which is already in ctree-internal format.*) (* val (h,argl) = strip_comb (str2term "Simplify (2*a + 3*a)"); val (h,argl) = strip_comb ((Thm.term_of o the o (parse (Thy_Info.get_theory "Simplify"))) "Simplify (2*a + 3*a)");