1.1 --- a/src/Tools/isac/BaseDefinitions/termC.sml	Mon Jun 21 15:36:09 2021 +0200
     1.2 +++ b/src/Tools/isac/BaseDefinitions/termC.sml	Mon Jun 21 15:42:53 2021 +0200
     1.3 @@ -429,8 +429,8 @@
     1.4  fun perm lhs rhs = var_perm (lhs, rhs) andalso not (lhs aconv rhs) andalso not (is_Var lhs);
     1.5  
     1.6  
     1.7 -fun pairT T1 T2 = Type ("*", [T1, T2]);
     1.8 -fun PairT T1 T2 = ([T1, T2] ---> Type ("*", [T1, T2]));
     1.9 +fun pairT T1 T2 = Type (\<^type_name>\<open>prod\<close>, [T1, T2]);
    1.10 +fun PairT T1 T2 = ([T1, T2] ---> Type (\<^type_name>\<open>prod\<close>, [T1, T2]));
    1.11  fun pairt t1 t2 = Const (\<^const_name>\<open>Pair\<close>, PairT (type_of t1) (type_of t2)) $ t1 $ t2;
    1.12  
    1.13  fun mk_factroot op_(*=thy.sqrt*) T fact root = 

     2.1 --- a/src/Tools/isac/Knowledge/Test.thy	Mon Jun 21 15:36:09 2021 +0200
     2.2 +++ b/src/Tools/isac/Knowledge/Test.thy	Mon Jun 21 15:42:53 2021 +0200
     2.3 @@ -44,13 +44,13 @@
     2.4  
     2.5  exception NO_EQUATION_TERM;
     2.6  fun is_equation ((Const (\<^const_name>\<open>HOL.eq\<close>,
     2.7 -    (Type (\<^type_name>\<open>fun\<close>, [Type (_, []), Type (\<^type_name>\<open>fun\<close>, [Type (_, []),Type ("bool",[])])])))) $ _ $ _) = true
     2.8 +    (Type (\<^type_name>\<open>fun\<close>, [Type (_, []), Type (\<^type_name>\<open>fun\<close>, [Type (_, []),Type (\<^type_name>\<open>bool\<close>,[])])])))) $ _ $ _) = true
     2.9    | is_equation _ = false;
    2.10  fun equ_lhs ((Const (\<^const_name>\<open>HOL.eq\<close>,
    2.11 -    (Type (\<^type_name>\<open>fun\<close>, [Type (_, []), Type (\<^type_name>\<open>fun\<close>, [Type (_, []),Type ("bool",[])])])))) $ l $ _) = l
    2.12 +    (Type (\<^type_name>\<open>fun\<close>, [Type (_, []), Type (\<^type_name>\<open>fun\<close>, [Type (_, []),Type (\<^type_name>\<open>bool\<close>,[])])])))) $ l $ _) = l
    2.13    | equ_lhs _ = raise NO_EQUATION_TERM;
    2.14  fun equ_rhs ((Const (\<^const_name>\<open>HOL.eq\<close>, (Type (\<^type_name>\<open>fun\<close>,
    2.15 -		 [Type (_, []), Type (\<^type_name>\<open>fun\<close>, [Type (_, []), Type ("bool",[])])])))) $ _ $ r) = r
    2.16 +		 [Type (_, []), Type (\<^type_name>\<open>fun\<close>, [Type (_, []), Type (\<^type_name>\<open>bool\<close>,[])])])))) $ _ $ r) = r
    2.17    | equ_rhs _ = raise NO_EQUATION_TERM;
    2.18  
    2.19  fun atom (Const (_, Type (_,[]))) = true

     3.1 --- a/test/Tools/isac/ProgLang/calculate.thy	Mon Jun 21 15:36:09 2021 +0200
     3.2 +++ b/test/Tools/isac/ProgLang/calculate.thy	Mon Jun 21 15:42:53 2021 +0200
     3.3 @@ -38,9 +38,9 @@
     3.4        (["Test", "test_calculate"],
     3.5          [("#Given" , ["realTestGiven t_t"]), ("#Find", ["realTestFind s_s"])],
     3.6          {rew_ord'="sqrt_right",rls'=tval_rls,srls = Rule_Set.empty, prls = Rule_Set.empty,
     3.7 -          calc=[("PLUS", ("op +", eval_binop "#add_")),
     3.8 +          calc=[("PLUS", (\<^const_name>\<open>plus\<close>, eval_binop "#add_")),
     3.9                ("TIMES", (\<^const_name>\<open>times\<close>, eval_binop "#mult_")),
    3.10 -              ("DIVIDE", ("HOL.divide", Prog_Expr.eval_cancel "#divide_")),
    3.11 +              ("DIVIDE", (\<^const_name>\<open>divide\<close>, Prog_Expr.eval_cancel "#divide_")),
    3.12                ("POWER", (\<^const_name>\<open>powr\<close>, eval_binop "#power_"))],
    3.13            crls=tval_rls, errpats = [], nrls= Rule_Set.empty (*, asm_rls=[],asm_thm=[]*)},
    3.14          @{thm calc_test.simps})]