1.1 --- a/src/Tools/isac/Interpret/li-tool.sml	Sat Aug 14 15:18:48 2021 +0200
     1.2 +++ b/src/Tools/isac/Interpret/li-tool.sml	Sat Aug 14 16:07:07 2021 +0200
     1.3 @@ -43,9 +43,7 @@
     1.4  
     1.5  (* find the formal argument of a tactic in case there is only one (e.g. in simplification) *)
     1.6  fun implicit_take (Rule.Prog prog) env =
     1.7 -      (case Prog_Tac.get_first_argument prog of
     1.8 -        NONE => NONE 
     1.9 -      | SOME prog_tac => SOME (subst_atomic env prog_tac))
    1.10 +    Option.map (subst_atomic env) (Prog_Tac.get_first_argument prog)
    1.11    | implicit_take _ _ = raise ERROR "implicit_take: no match";
    1.12  
    1.13  (*  *)

     2.1 --- a/src/Tools/isac/Knowledge/Rational.thy	Sat Aug 14 15:18:48 2021 +0200
     2.2 +++ b/src/Tools/isac/Knowledge/Rational.thy	Sat Aug 14 16:07:07 2021 +0200
     2.3 @@ -237,7 +237,7 @@
     2.4  
     2.5  (* prepare a term for cancellation by factoring out the gcd
     2.6    assumes: is a fraction with outmost "/"*)
     2.7 -fun factout_p_ (thy: theory) t =
     2.8 +fun factout_p_ (_: theory) t =
     2.9    let val opt = check_fraction t
    2.10    in
    2.11      case opt of