1.1 --- a/src/Tools/isac/MathEngBasic/tactic.sml	Fri Jan 17 12:37:21 2020 +0100
     1.2 +++ b/src/Tools/isac/MathEngBasic/tactic.sml	Fri Jan 17 13:14:11 2020 +0100
     1.3 @@ -311,7 +311,7 @@
     1.4    | rls_of (Rewrite_Set rls) = rls
     1.5    | rls_of input = error ("rls_of: called with input \"" ^ tac2IDstr input ^ "\"");
     1.6  
     1.7 -fun rule2tac thy _ (Rule.Calc (opID, _)) = Calculate (assoc_calc thy opID)
     1.8 +fun rule2tac thy _ (Rule.Num_Calc (opID, _)) = Calculate (assoc_calc thy opID)
     1.9    | rule2tac _ [] (Rule.Thm thm'') = Rewrite thm''
    1.10    | rule2tac _ subst (Rule.Thm thm'') = 
    1.11      Rewrite_Inst (Selem.subst2subs subst, thm'')