1.1 --- a/src/Tools/isac/Knowledge/Equation.thy	Mon Jun 21 14:39:52 2021 +0200
     1.2 +++ b/src/Tools/isac/Knowledge/Equation.thy	Mon Jun 21 15:36:09 2021 +0200
     1.3 @@ -61,7 +61,7 @@
     1.4     val (h,argl) = strip_comb ((Thm.term_of o the o (parse thy)) 
     1.5  				  "solveTest (x+1=2, x)");
     1.6     *)
     1.7 -fun argl2dtss [Const ("Product_Type.Pair", _) $ eq $ bdv] =
     1.8 +fun argl2dtss [Const (\<^const_name>\<open>Pair\<close>, _) $ eq $ bdv] =
     1.9      [((the o (TermC.parseNEW \<^context>)) "equality", [eq]),
    1.10       ((the o (TermC.parseNEW \<^context>)) "solveFor", [bdv]),
    1.11       ((the o (TermC.parseNEW \<^context>)) "solutions",