1.1 --- a/src/Tools/isac/Knowledge/Equation.thy Tue May 03 16:23:07 2011 +0200
1.2 +++ b/src/Tools/isac/Knowledge/Equation.thy Wed May 04 09:01:10 2011 +0200
1.3 @@ -68,7 +68,7 @@
1.4 val (h,argl) = strip_comb ((term_of o the o (parse thy))
1.5 "solveTest (x+1=2, x)");
1.6 *)
1.7 -fun argl2dtss [Const ("Pair", _) $ eq $ bdv] =
1.8 +fun argl2dtss [Const ("Product_Type.Pair", _) $ eq $ bdv] =
1.9 [((the o (parseNEW ctxt)) "equality", [eq]),
1.10 ((the o (parseNEW ctxt)) "solveFor", [bdv]),
1.11 ((the o (parseNEW ctxt)) "solutions",