diff -r 995177b6d786 -r eff0b9fc6caa src/Tools/isac/Knowledge/Rational.thy
--- a/src/Tools/isac/Knowledge/Rational.thy	Tue Apr 14 15:56:15 2020 +0200
+++ b/src/Tools/isac/Knowledge/Rational.thy	Wed Apr 15 10:07:43 2020 +0200
@@ -485,15 +485,15 @@
   in (t, t'', [rs(*one in order to ease locate_rule*)], der) end;
 
 fun locate_rule thy eval_rls ro [rs] t r =
-    if member op = ((map (ThmC.id_of_thm)) rs) (ThmC.id_of_thm r)
+    if member op = ((map (Rule.thm_id)) rs) (Rule.thm_id r)
     then 
-      let val ropt = Rewrite.rewrite_ thy ro eval_rls true (ThmC.thm_of_thm r) t;
+      let val ropt = Rewrite.rewrite_ thy ro eval_rls true (Rule.thm r) t;
       in
         case ropt of SOME ta => [(r, ta)]
 	      | NONE => ((*tracing 
-	          ("### locate_rule:  rewrite " ^ ThmC.id_of_thm r ^ " " ^ UnparseC.term t ^ " = NONE");*) []) 
+	          ("### locate_rule:  rewrite " ^ Rule.thm_id r ^ " " ^ UnparseC.term t ^ " = NONE");*) []) 
 			end
-    else ((*tracing ("### locate_rule:  " ^ ThmC.id_of_thm r ^ " not mem rrls");*) [])
+    else ((*tracing ("### locate_rule:  " ^ Rule.thm_id r ^ " not mem rrls");*) [])
   | locate_rule _ _ _ _ _ _ = error "locate_rule: doesnt match rev-sets in istate";
 
 fun next_rule thy eval_rls ro [rs] t =
@@ -546,16 +546,16 @@
   in (t, t'', [rs(*here only _ONE_*)], der) end;
 
 fun locate_rule thy eval_rls ro [rs] t r =
-    if member op = ((map (ThmC.id_of_thm)) rs) (ThmC.id_of_thm r)
+    if member op = ((map (Rule.thm_id)) rs) (Rule.thm_id r)
     then 
-      let val ropt = Rewrite.rewrite_ thy ro eval_rls true (ThmC.thm_of_thm r) t;
+      let val ropt = Rewrite.rewrite_ thy ro eval_rls true (Rule.thm r) t;
       in 
         case ropt of
           SOME ta => [(r, ta)]
 	      | NONE => 
-	        ((*tracing ("### locate_rule:  rewrite " ^ ThmC.id_of_thm r ^ " " ^ UnparseC.term t ^ " = NONE");*)
+	        ((*tracing ("### locate_rule:  rewrite " ^ Rule.thm_id r ^ " " ^ UnparseC.term t ^ " = NONE");*)
 	        []) end
-    else ((*tracing ("### locate_rule:  " ^ ThmC.id_of_thm r ^ " not mem rrls");*) [])
+    else ((*tracing ("### locate_rule:  " ^ Rule.thm_id r ^ " not mem rrls");*) [])
   | locate_rule _ _ _ _ _ _ = error "locate_rule: doesnt match rev-sets in istate";
 
 fun next_rule thy eval_rls ro [rs] t =