1.1 --- a/src/Tools/isac/Knowledge/Base_Tools.thy Thu Apr 09 17:16:48 2020 +0200
1.2 +++ b/src/Tools/isac/Knowledge/Base_Tools.thy Thu Apr 09 18:21:09 2020 +0200
1.3 @@ -42,8 +42,8 @@
1.4 local
1.5 open Term;
1.6 in
1.7 - fun termlessI (_: Rule.subst) uv = LibraryC.termless uv;
1.8 - fun term_ordI (_: Rule.subst) uv = Term_Ord.term_ord uv;
1.9 + fun termlessI (_: UnparseC.subst) uv = LibraryC.termless uv;
1.10 + fun term_ordI (_: UnparseC.subst) uv = Term_Ord.term_ord uv;
1.11 end;
1.12 \<close> ML \<open>
1.13 (*TODO.WN0509 reduce ids: tless_true = e_rew_ord' = Rewrite_Ord.e_rew_ord = Rewrite_Ord.dummy_ord*)