diff -r a474900d5bd2 -r 255c853ea2f0 src/Tools/isac/Knowledge/Equation.thy
--- a/src/Tools/isac/Knowledge/Equation.thy	Thu Dec 22 11:12:18 2016 +0100
+++ b/src/Tools/isac/Knowledge/Equation.thy	Thu Dec 22 11:36:20 2016 +0100
@@ -65,7 +65,7 @@
 
 ML{*
 (*.function for handling the cas-input "solve (x+1=2, x)":
-   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 "solve (x+1=2, x)");
    val (h,argl) = strip_comb ((Thm.term_of o the o (parse thy)) 
 				  "solveTest (x+1=2, x)");