1.1 --- a/src/Tools/isac/BaseDefinitions/rule.sml	Mon Apr 27 16:40:11 2020 +0200
     1.2 +++ b/src/Tools/isac/BaseDefinitions/rule.sml	Tue Apr 28 15:31:49 2020 +0200
     1.3 @@ -18,6 +18,8 @@
     1.4    val to_string_short: Rule_Def.rule -> string
     1.5  
     1.6    val thm: rule -> thm
     1.7 +  val distinct : rule list -> rule list
     1.8 +
     1.9  (* ---- for tests only: shifted from below to remove the Warning "unused" at fun.def. --------- *)
    1.10    val thm_id: rule -> string
    1.11  (*/-------------------------------------------------------- ! aktivate for Test_Isac BEGIN ---\* )
    1.12 @@ -52,6 +54,7 @@
    1.13    | equal (Rule_Def.Eval (id1, _), Rule_Def.Eval (id2, _)) = id1 = id2
    1.14    | equal (Rule_Def.Rls_ rls1, Rule_Def.Rls_ rls2) = set_id rls1 = set_id rls2
    1.15    | equal _ = false;
    1.16 +fun distinct rs = Library.distinct equal rs
    1.17  
    1.18  fun to_string Rule_Def.Erule = "Erule" 
    1.19    | to_string (Rule_Def.Thm (str, thm)) = "Thm (\"" ^ str ^ "\"," ^ ThmC_Def.string_of_thm thm ^ ")"