src/Tools/isac/Knowledge/Equation.thy
branchdecompose-isar
changeset 41972 22c5483e9bfb
parent 41952 0e76e17a430a
child 42398 04d3f0133827
     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",