1.1 --- a/src/Tools/isac/Knowledge/PolyEq.thy	Tue Apr 27 18:09:22 2021 +0200
     1.2 +++ b/src/Tools/isac/Knowledge/PolyEq.thy	Tue Apr 27 18:14:02 2021 +0200
     1.3 @@ -1154,13 +1154,14 @@
     1.4    | pr_ord LESS  = "LESS"
     1.5    | pr_ord GREATER = "GREATER";
     1.6  
     1.7 -fun dest_hd' x (Const (a, T)) = (((a, 0), T), 0)
     1.8 +fun dest_hd' _ (Const (a, T)) = (((a, 0), T), 0)
     1.9    | dest_hd' x (t as Free (a, T)) =
    1.10      if x = t then ((("|||||||||||||", 0), T), 0)                        (*WN*)
    1.11      else (((a, 0), T), 1)
    1.12 -  | dest_hd' x (Var v) = (v, 2)
    1.13 -  | dest_hd' x (Bound i) = ((("", i), dummyT), 3)
    1.14 -  | dest_hd' x (Abs (_, T, _)) = ((("", 0), T), 4);
    1.15 +  | dest_hd' _ (Var v) = (v, 2)
    1.16 +  | dest_hd' _ (Bound i) = ((("", i), dummyT), 3)
    1.17 +  | dest_hd' _ (Abs (_, T, _)) = ((("", 0), T), 4)
    1.18 +  | dest_hd' _ _ = raise ERROR "dest_hd': uncovered case in fun.def.";
    1.19  
    1.20  fun size_of_term' x (Const ("Prog_Expr.pow",_) $ Free (var,_) $ Free (pot,_)) =
    1.21      (case x of                                                          (*WN*)
    1.22 @@ -1175,7 +1176,7 @@
    1.23  			  (UnparseC.term x)))
    1.24    | size_of_term' x (Abs (_,_,body)) = 1 + size_of_term' x body
    1.25    | size_of_term' x (f$t) = size_of_term' x f  +  size_of_term' x t
    1.26 -  | size_of_term' x _ = 1;
    1.27 +  | size_of_term' _ _ = 1;
    1.28  
    1.29  fun term_ord' x pr thy (Abs (_, T, t), Abs(_, U, u)) =       (* ~ term.ML *)
    1.30      (case term_ord' x pr thy (t, u) of EQUAL => Term_Ord.typ_ord (T, U) | ord => ord)
    1.31 @@ -1207,20 +1208,17 @@
    1.32  and hd_ord x (f, g) =                                        (* ~ term.ML *)
    1.33    prod_ord (prod_ord Term_Ord.indexname_ord Term_Ord.typ_ord) 
    1.34              int_ord (dest_hd' x f, dest_hd' x g)
    1.35 -and terms_ord x str pr (ts, us) = 
    1.36 +and terms_ord x _ pr (ts, us) = 
    1.37      list_ord (term_ord' x pr (ThyC.get_theory "Isac_Knowledge"))(ts, us);
    1.38  
    1.39  in
    1.40  
    1.41 -fun ord_make_polynomial_in (pr:bool) thy subst tu = 
    1.42 -    let
    1.43 -	(* val _=tracing("*** subs variable is: "^(Env.subst2str subst)); *)
    1.44 -    in
    1.45 +fun ord_make_polynomial_in (pr:bool) thy subst tu =
    1.46 +  ((**)tracing ("*** subs variable is: " ^ (Env.subst2str subst)); (**)
    1.47  	case subst of
    1.48 -	    (_,x)::_ => (term_ord' x pr thy tu = LESS)
    1.49 -	  | _ => raise ERROR ("ord_make_polynomial_in called with subst = "^
    1.50 -			  (Env.subst2str subst))
    1.51 -    end;
    1.52 +	  (_, x) :: _ => (term_ord' x pr thy tu = LESS)
    1.53 +	| _ => raise ERROR ("ord_make_polynomial_in called with subst = " ^ Env.subst2str subst))
    1.54 +
    1.55  end;(*local*)
    1.56  
    1.57  \<close>

     2.1 --- a/src/Tools/isac/MathEngBasic/rewrite.sml	Tue Apr 27 18:09:22 2021 +0200
     2.2 +++ b/src/Tools/isac/MathEngBasic/rewrite.sml	Tue Apr 27 18:14:02 2021 +0200
     2.3 @@ -291,7 +291,7 @@
     2.4           SOME (rew, _) => rew
     2.5         | NONE => raise ERROR ""
     2.6       in SOME (rew, (thmID, thm)) end)
     2.7 -	   handle _ (*TODO Pattern.MATCH ?del?*)=> raise ERROR ("calculate_: " ^ thmID ^ " does not rewrite")
     2.8 +	   handle NO_REWRITE => raise ERROR ("calculate_: " ^ thmID ^ " does not rewrite")
     2.9    end;
    2.10  
    2.11  fun eval_prog_expr thy srls t =