1.1 --- a/src/Tools/isac/Knowledge/EqSystem.thy	Thu Apr 29 12:43:50 2021 +0200
     1.2 +++ b/src/Tools/isac/Knowledge/EqSystem.thy	Thu Apr 29 14:13:11 2021 +0200
     1.3 @@ -108,7 +108,8 @@
     1.4        | _ => (((ccc, 0), T), 1))
     1.5    | dest_hd' (Var v) = (v, 2)
     1.6    | dest_hd' (Bound i) = ((("", i), dummyT), 3)
     1.7 -  | dest_hd' (Abs (_, T, _)) = ((("", 0), T), 4);
     1.8 +  | dest_hd' (Abs (_, T, _)) = ((("", 0), T), 4)
     1.9 +  | dest_hd' _ = raise ERROR "dest_hd': uncovered case in fun.def.";
    1.10  
    1.11  fun size_of_term' (Free (ccc, _)) =
    1.12      (case Symbol.explode ccc of (*WN0510 hack for the bound variables*)
    1.13 @@ -147,7 +148,7 @@
    1.14  	 | ord => ord)
    1.15  and hd_ord (f, g) =                                        (* ~ term.ML *)
    1.16    prod_ord (prod_ord Term_Ord.indexname_ord Term_Ord.typ_ord) int_ord (dest_hd' f, dest_hd' g)
    1.17 -and terms_ord str pr (ts, us) = list_ord (term_ord' pr (ThyC.get_theory "Isac_Knowledge"))(ts, us);
    1.18 +and terms_ord _ pr (ts, us) = list_ord (term_ord' pr (ThyC.get_theory "Isac_Knowledge"))(ts, us);
    1.19  (**)
    1.20  in
    1.21  (**)
    1.22 @@ -156,7 +157,7 @@
    1.23      (term_ord' pr thy (Library.swap tu) = LESS);*)
    1.24  
    1.25  (*for the rls's*)
    1.26 -fun ord_simplify_System (pr:bool) thy subst tu = 
    1.27 +fun ord_simplify_System (pr:bool) thy _(*subst*) tu = 
    1.28      (term_ord' pr thy tu = LESS);
    1.29  (**)
    1.30  end;