1.1 --- a/src/Tools/isac/Knowledge/LinEq.thy Fri Jun 13 09:55:49 2014 +0200
1.2 +++ b/src/Tools/isac/Knowledge/LinEq.thy Fri Jun 13 10:29:06 2014 +0200
1.3 @@ -75,7 +75,7 @@
1.4 [("LinEq_erls", (Context.theory_name @{theory}, LinEq_erls))] *}
1.5 ML {*
1.6
1.7 -val LinPoly_simplify = prep_rls(
1.8 +val LinPoly_simplify = prep_rls'(
1.9 Rls {id = "LinPoly_simplify", preconds = [],
1.10 rew_ord = ("termlessI",termlessI),
1.11 erls = LinEq_erls,
1.12 @@ -99,7 +99,7 @@
1.13 ML {*
1.14
1.15 (*isolate the bound variable in an linear equation; 'bdv' is a meta-constant*)
1.16 -val LinEq_simplify = prep_rls(
1.17 +val LinEq_simplify = prep_rls'(
1.18 Rls {id = "LinEq_simplify", preconds = [],
1.19 rew_ord = ("e_rew_ord",e_rew_ord),
1.20 erls = LinEq_erls,