1.1 --- a/src/Tools/isac/Knowledge/Equation.thy	Mon Dec 07 10:52:07 2015 +0100
     1.2 +++ b/src/Tools/isac/Knowledge/Equation.thy	Mon Dec 07 11:25:02 2015 +0100
     1.3 @@ -67,7 +67,7 @@
     1.4  (*.function for handling the cas-input "solve (x+1=2, x)":
     1.5     make a model which is already in ptree-internal format.*)
     1.6  (* val (h,argl) = strip_comb (str2term "solve (x+1=2, x)");
     1.7 -   val (h,argl) = strip_comb ((term_of o the o (parse thy)) 
     1.8 +   val (h,argl) = strip_comb ((Thm.term_of o the o (parse thy)) 
     1.9  				  "solveTest (x+1=2, x)");
    1.10     *)
    1.11  fun argl2dtss [Const ("Product_Type.Pair", _) $ eq $ bdv] =
    1.12 @@ -79,9 +79,9 @@
    1.13    | argl2dtss _ = error "Equation.ML: wrong argument for argl2dtss";
    1.14  *}
    1.15  setup {* KEStore_Elems.add_cas
    1.16 -  [((term_of o the o (parse thy)) "solveTest", 
    1.17 +  [((Thm.term_of o the o (parse thy)) "solveTest", 
    1.18        (("Test", ["univariate","equation","test"], ["no_met"]), argl2dtss)),
    1.19 -    ((term_of o the o (parse thy)) "solve",
    1.20 +    ((Thm.term_of o the o (parse thy)) "solve",
    1.21        (("Isac", ["univariate","equation"], ["no_met"]), argl2dtss))]*}
    1.22  
    1.23