src/Tools/isac/MathEngBasic/tactic.sml
changeset 59878 3163e63a5111
parent 59874 820bf0840029
child 59879 33449c96d99f
     1.1 --- a/src/Tools/isac/MathEngBasic/tactic.sml	Wed Apr 15 11:11:54 2020 +0200
     1.2 +++ b/src/Tools/isac/MathEngBasic/tactic.sml	Wed Apr 15 11:37:43 2020 +0200
     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.Num_Calc (opID, _)) = Calculate (assoc_calc thy opID)
     1.8 +fun rule2tac thy _ (Rule.Eval (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'')