src/Tools/isac/CalcElements/rule-set.sml
changeset 59858 a2c32a38327a
parent 59857 cbb3fae0381d
child 59861 65ec9f679c3f
     1.1 --- a/src/Tools/isac/CalcElements/rule-set.sml	Wed Apr 08 16:56:47 2020 +0200
     1.2 +++ b/src/Tools/isac/CalcElements/rule-set.sml	Thu Apr 09 11:21:53 2020 +0200
     1.3 @@ -165,7 +165,7 @@
     1.4    | eq_rule _ = false;
     1.5  
     1.6  fun rule2str Rule_Def.Erule = "Erule" 
     1.7 -  | rule2str (Rule_Def.Thm (str, thm)) = "Thm (\"" ^ str ^ "\"," ^ Rule.string_of_thmI thm ^ ")"
     1.8 +  | rule2str (Rule_Def.Thm (str, thm)) = "Thm (\"" ^ str ^ "\"," ^ ThmC.string_of_thmI thm ^ ")"
     1.9    | rule2str (Rule_Def.Num_Calc (str, _)) = "Num_Calc (\"" ^ str ^ "\",fn)"
    1.10    | rule2str (Rule_Def.Cal1 (str, _)) = "Cal1 (\"" ^ str ^ "\",fn)"
    1.11    | rule2str (Rule_Def.Rls_ rls) = "Rls_ (\"" ^ id_rls rls ^ "\")";