1.1 --- a/src/Tools/isac/Knowledge/Rational-WN.sml	Fri Apr 10 12:28:47 2020 +0200
     1.2 +++ b/src/Tools/isac/Knowledge/Rational-WN.sml	Fri Apr 10 14:46:55 2020 +0200
     1.3 @@ -195,7 +195,7 @@
     1.4        case rul of
     1.5  	Rule.Thm (thmid, thm) =>
     1.6  	  (case rewrite_ thy ((snd o #rew_ord o Rule_Set.rep) ruless) 
     1.7 -	     rls put_asm (ThmC.thm_of_thm rul) ct of
     1.8 +	     rls put_asm (ThmC_Def.thm_of_thm rul) ct of
     1.9  	     NONE => rew_once ruls asm ct apno thms
    1.10  	   | SOME (ct',asm') => 
    1.11  	     rew_once ruls (asm union asm') ct' Appl (rul::thms))
    1.12 @@ -209,7 +209,7 @@
    1.13  		   rls put_asm thm' ct;
    1.14  		 val _ = if pairopt <> NONE then () 
    1.15  			 else error("rewrite_set_, rewrite_ \""^
    1.16 -			 (ThmC.string_of_thmI thm')^"\" \""^
    1.17 +			 (ThmC_Def.string_of_thmI thm')^"\" \""^
    1.18  			 (Syntax.string_of_term (ThyC.thy2ctxt thy) ct)^"\" = NONE")
    1.19  	       in rew_once ruls asm ((fst o the) pairopt) Appl(rul::thms) end);
    1.20      val ruls = (#rules o Rule_Set.rep) ruless;
    1.21 @@ -231,7 +231,7 @@
    1.22        case rul of
    1.23  	Rule.Thm (thmid, thm) =>
    1.24  	  (case rewrite_ thy ((snd o #rew_ord o Rule_Set.rep) ruless) 
    1.25 -	     rls put_asm (ThmC.thm_of_thm rul) ct of
    1.26 +	     rls put_asm (ThmC_Def.thm_of_thm rul) ct of
    1.27  	     NONE => rew_once ruls asm ct apno thms
    1.28  	   | SOME (ct',asm') => 
    1.29  	     rew_once ruls (asm union asm') ct' Appl (rul::thms))
    1.30 @@ -245,7 +245,7 @@
    1.31  		   rls put_asm thm' ct;
    1.32  		 val _ = if pairopt <> NONE then () 
    1.33  			 else error("rewrite_set_, rewrite_ \""^
    1.34 -			 (ThmC.string_of_thmI thm')^"\" \""^
    1.35 +			 (ThmC_Def.string_of_thmI thm')^"\" \""^
    1.36  			 (Syntax.string_of_term (ThyC.thy2ctxt thy) ct)^"\" = NONE")
    1.37  	       in rew_once ruls asm ((fst o the) pairopt) Appl(rul::thms) end);
    1.38      val ruls = (#rules o Rule_Set.rep) ruless;