1.1 --- a/src/Tools/isac/Knowledge/Rational.thy	Tue Apr 14 15:56:15 2020 +0200
     1.2 +++ b/src/Tools/isac/Knowledge/Rational.thy	Wed Apr 15 10:07:43 2020 +0200
     1.3 @@ -485,15 +485,15 @@
     1.4    in (t, t'', [rs(*one in order to ease locate_rule*)], der) end;
     1.5  
     1.6  fun locate_rule thy eval_rls ro [rs] t r =
     1.7 -    if member op = ((map (ThmC.id_of_thm)) rs) (ThmC.id_of_thm r)
     1.8 +    if member op = ((map (Rule.thm_id)) rs) (Rule.thm_id r)
     1.9      then 
    1.10 -      let val ropt = Rewrite.rewrite_ thy ro eval_rls true (ThmC.thm_of_thm r) t;
    1.11 +      let val ropt = Rewrite.rewrite_ thy ro eval_rls true (Rule.thm r) t;
    1.12        in
    1.13          case ropt of SOME ta => [(r, ta)]
    1.14  	      | NONE => ((*tracing 
    1.15 -	          ("### locate_rule:  rewrite " ^ ThmC.id_of_thm r ^ " " ^ UnparseC.term t ^ " = NONE");*) []) 
    1.16 +	          ("### locate_rule:  rewrite " ^ Rule.thm_id r ^ " " ^ UnparseC.term t ^ " = NONE");*) []) 
    1.17  			end
    1.18 -    else ((*tracing ("### locate_rule:  " ^ ThmC.id_of_thm r ^ " not mem rrls");*) [])
    1.19 +    else ((*tracing ("### locate_rule:  " ^ Rule.thm_id r ^ " not mem rrls");*) [])
    1.20    | locate_rule _ _ _ _ _ _ = error "locate_rule: doesnt match rev-sets in istate";
    1.21  
    1.22  fun next_rule thy eval_rls ro [rs] t =
    1.23 @@ -546,16 +546,16 @@
    1.24    in (t, t'', [rs(*here only _ONE_*)], der) end;
    1.25  
    1.26  fun locate_rule thy eval_rls ro [rs] t r =
    1.27 -    if member op = ((map (ThmC.id_of_thm)) rs) (ThmC.id_of_thm r)
    1.28 +    if member op = ((map (Rule.thm_id)) rs) (Rule.thm_id r)
    1.29      then 
    1.30 -      let val ropt = Rewrite.rewrite_ thy ro eval_rls true (ThmC.thm_of_thm r) t;
    1.31 +      let val ropt = Rewrite.rewrite_ thy ro eval_rls true (Rule.thm r) t;
    1.32        in 
    1.33          case ropt of
    1.34            SOME ta => [(r, ta)]
    1.35  	      | NONE => 
    1.36 -	        ((*tracing ("### locate_rule:  rewrite " ^ ThmC.id_of_thm r ^ " " ^ UnparseC.term t ^ " = NONE");*)
    1.37 +	        ((*tracing ("### locate_rule:  rewrite " ^ Rule.thm_id r ^ " " ^ UnparseC.term t ^ " = NONE");*)
    1.38  	        []) end
    1.39 -    else ((*tracing ("### locate_rule:  " ^ ThmC.id_of_thm r ^ " not mem rrls");*) [])
    1.40 +    else ((*tracing ("### locate_rule:  " ^ Rule.thm_id r ^ " not mem rrls");*) [])
    1.41    | locate_rule _ _ _ _ _ _ = error "locate_rule: doesnt match rev-sets in istate";
    1.42  
    1.43  fun next_rule thy eval_rls ro [rs] t =