1.1 --- a/src/Tools/isac/Knowledge/Base_Tools.thy	Fri Apr 24 08:51:05 2020 +0200
     1.2 +++ b/src/Tools/isac/Knowledge/Base_Tools.thy	Fri Apr 24 09:01:48 2020 +0200
     1.3 @@ -42,8 +42,8 @@
     1.4  local
     1.5    open Term;
     1.6  in
     1.7 -  fun termlessI (_: UnparseC.subst) uv = LibraryC.termless uv;
     1.8 -  fun term_ordI (_: UnparseC.subst) uv = Term_Ord.term_ord uv;
     1.9 +  fun termlessI (_: subst) uv = LibraryC.termless uv;
    1.10 +  fun term_ordI (_: 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*)