1.1 --- a/src/Tools/isac/Knowledge/Equation.thy	Thu Apr 07 16:31:05 2011 +0200
     1.2 +++ b/src/Tools/isac/Knowledge/Equation.thy	Fri Apr 08 15:16:08 2011 +0200
     1.3 @@ -29,6 +29,7 @@
     1.4  
     1.5  ML {*
     1.6  val thy = @{theory};
     1.7 +val ctxt = thy2ctxt thy;
     1.8  
     1.9  val univariate_equation_prls = 
    1.10      append_rls "univariate_equation_prls" e_rls 
    1.11 @@ -68,10 +69,10 @@
    1.12  				  "solveTest (x+1=2, x)");
    1.13     *)
    1.14  fun argl2dtss [Const ("Pair", _) $ eq $ bdv] =
    1.15 -    [((term_of o the o (parse thy)) "equality", [eq]),
    1.16 -     ((term_of o the o (parse thy)) "solveFor", [bdv]),
    1.17 -     ((term_of o the o (parse thy)) "solutions", 
    1.18 -      [(term_of o the o (parse thy)) "L"])
    1.19 +    [((the o (parseNEW ctxt)) "equality", [eq]),
    1.20 +     ((the o (parseNEW ctxt)) "solveFor", [bdv]),
    1.21 +     ((the o (parseNEW ctxt)) "solutions", 
    1.22 +      [(the o (parseNEW ctxt)) "L"])
    1.23       ]
    1.24    | argl2dtss _ = error "Equation.ML: wrong argument for argl2dtss";
    1.25