src/Tools/isac/Knowledge/Equation.thy
changeset 59962 6a59d252345d
parent 59903 5037ca1b112b
child 59973 8a46c2e7c27a
     1.1 --- a/src/Tools/isac/Knowledge/Equation.thy	Mon May 11 11:22:46 2020 +0200
     1.2 +++ b/src/Tools/isac/Knowledge/Equation.thy	Mon May 11 11:38:52 2020 +0200
     1.3 @@ -71,7 +71,7 @@
     1.4       ((the o (TermC.parseNEW ctxt)) "solutions", 
     1.5        [(the o (TermC.parseNEW ctxt)) "L"])
     1.6       ]
     1.7 -  | argl2dtss _ = error "Equation.ML: wrong argument for argl2dtss";
     1.8 +  | argl2dtss _ = raise ERROR "Equation.ML: wrong argument for argl2dtss";
     1.9  \<close>
    1.10  setup \<open>KEStore_Elems.add_cas
    1.11    [((Thm.term_of o the o (TermC.parse thy)) "solveTest",