1.1 --- a/test/Tools/isac/ProgLang/evaluate.sml	Mon Jun 21 14:39:52 2021 +0200
     1.2 +++ b/test/Tools/isac/ProgLang/evaluate.sml	Mon Jun 21 15:36:09 2021 +0200
     1.3 @@ -45,10 +45,10 @@
     1.4  (* fun rewrite__set_ \<longrightarrow> fun rew_once works the same way *)
     1.5  val t = TermC.str2term "((1+2)*4/3) \<up> 2";
     1.6  val thy = @{theory};
     1.7 -val times =  ("Groups.times_class.times", eval_binop "#mult_") : string * Eval_Def.eval_fn;
     1.8 -val plus =   ("Groups.plus_class.plus",eval_binop "#add_") : string * Eval_Def.eval_fn;
     1.9 -val divide = ("Rings.divide_class.divide"  ,eval_cancel "#divide_e") : string * Eval_Def.eval_fn;
    1.10 -val pow =    ("Transcendental.powr"  ,eval_binop "#power_") : string * Eval_Def.eval_fn;
    1.11 +val times =  (\<^const_name>\<open>times\<close>, eval_binop "#mult_") : string * Eval_Def.eval_fn;
    1.12 +val plus =   (\<^const_name>\<open>plus\<close>,eval_binop "#add_") : string * Eval_Def.eval_fn;
    1.13 +val divide = (\<^const_name>\<open>divide\<close>  ,eval_cancel "#divide_e") : string * Eval_Def.eval_fn;
    1.14 +val pow =    (\<^const_name>\<open>powr\<close>  ,eval_binop "#power_") : string * Eval_Def.eval_fn;
    1.15  
    1.16  "~~~~~ fun calculate_, args:"; val (thy, isa_fn, t) = (thy, plus, t);
    1.17  val SOME ("#: 1 + 2 = 3", adh_thm) = adhoc_thm @{theory} isa_fn t;
    1.18 @@ -137,7 +137,7 @@
    1.19   val t = (Thm.term_of o the o (TermC.parse @{theory Test})) "2 is_const";
    1.20   TermC.atomty t;
    1.21   rewrite_set_ @{theory Test} false tval_rls t;
    1.22 -(*val it = SOME (Const ("HOL.True", "bool"),[]) ... works*)
    1.23 +(*val it = SOME (Const (\<^const_name>\<open>True\<close>, "bool"),[]) ... works*)
    1.24  
    1.25   val t = TermC.str2term "2 * x is_const";
    1.26   val SOME (str,t') = eval_const "" "" t (@{theory "Isac_Knowledge"});
    1.27 @@ -153,7 +153,7 @@
    1.28   val rls = Test_simplify;
    1.29   val t = (Thm.term_of o the o (TermC.parse thy)) "(-4) / 2";
    1.30  
    1.31 -val SOME (_, t) = eval_cancel "xxx" "Rings.divide_class.divide" t thy;
    1.32 +val SOME (_, t) = eval_cancel "xxx" \<^const_name>\<open>divide\<close> t thy;
    1.33  
    1.34  (*--------------(5): reproduce (1) with simpler term: ------------*)
    1.35   val t = (Thm.term_of o the o (TermC.parse thy)) "(3+5)/2";
    1.36 @@ -163,7 +163,7 @@
    1.37  
    1.38   val t = (Thm.term_of o the o (TermC.parse thy)) "(3+1+2*x)/2";
    1.39  case rewrite_set_ thy false rls t of
    1.40 -  SOME (Const ("Groups.plus_class.plus", _) $ Free ("2", _) $ Free ("x", _), []) => ()
    1.41 +  SOME (Const (\<^const_name>\<open>plus\<close>, _) $ Free ("2", _) $ Free ("x", _), []) => ()
    1.42  | _ => error "rewrite_set_ (3+1+2*x)/2 changed";
    1.43  
    1.44   Rewrite.trace_on:=false; (*=true3.6.03*)
    1.45 @@ -282,7 +282,7 @@
    1.46  
    1.47    val (op_, eval_fn) = the (LibraryC.assoc(KEStore_Elems.get_calcs @{theory},"POWER"));
    1.48    (*
    1.49 -val op_ = "Transcendental.powr" : string
    1.50 +val op_ = \<^const_name>\<open>powr\<close> : string
    1.51  val eval_fn = fn : string -> term -> theory -> (string * term) option*)
    1.52  
    1.53    val SOME (thmid,t') = get_pair thy op_ eval_fn t;
    1.54 @@ -321,7 +321,7 @@
    1.55  
    1.56  val SOME (t',_) = rewrite_set_ @{theory Test} false tval_rls t;
    1.57  UnparseC.term t';
    1.58 -"HOL.False";
    1.59 +\<^const_name>\<open>False\<close>;
    1.60  
    1.61  "----------- fun get_pair: examples ------------------------------------------------------------";
    1.62  "----------- fun get_pair: examples ------------------------------------------------------------";
    1.63 @@ -374,7 +374,7 @@
    1.64  then () else error "adhoc_thm  9 is_const  changed";
    1.65  
    1.66  
    1.67 -case assoc_calc thy "Orderings.ord_class.less" of
    1.68 +case assoc_calc thy \<^const_name>\<open>less\<close> of
    1.69    "le" => () | _ => error "Orderings.ord_class.less <-> le changed";
    1.70  (*--------------------------------------------------------------------vvvvvvvvvv*)
    1.71  val SOME (isa_str, eval_fn) = LibraryC.assoc (KEStore_Elems.get_calcs @{theory}, "le");