1.1 --- a/src/Tools/isac/Knowledge/InsSort.thy	Wed Apr 15 11:11:54 2020 +0200
     1.2 +++ b/src/Tools/isac/Knowledge/InsSort.thy	Wed Apr 15 11:37:43 2020 +0200
     1.3 @@ -62,11 +62,11 @@
     1.4  	    Rule.Thm ("o_apply", @{thm o_apply} (* (?f \<circ> ?g) ?x = ?f (?g ?x) *)),
     1.5  	    Rule.Thm ("id_apply", @{thm id_apply} (* id ?x = ?x *)),
     1.6        
     1.7 -	    Rule.Num_Calc ("Orderings.ord_class.less", Prog_Expr.eval_equ "#less_"),
     1.8 +	    Rule.Eval ("Orderings.ord_class.less", Prog_Expr.eval_equ "#less_"),
     1.9  	    Rule.Thm ("If_def", @{thm If_def} (* if ?P then ?x else ?y \<equiv> THE z. (?P = True \<longrightarrow> z = ?x) \<and> (?P = False \<longrightarrow> z = ?y) *)),
    1.10  	    Rule.Thm ("if_True", @{thm if_True} (* "(if True then x else y) = x" *)),
    1.11  	    Rule.Thm ("if_False", @{thm if_False} (* "(if False then x else y) = y" *))],
    1.12 -	  errpatts = [], scr = Rule.EmptyScr};      
    1.13 +	  errpatts = [], scr = Rule.Empty_Prog};      
    1.14  \<close>
    1.15  setup \<open>KEStore_Elems.add_rlss [("ins_sort", (Context.theory_name @{theory}, ins_sort))]\<close>
    1.16