1.1 --- a/test/Tools/isac/BridgeLibisabelle/mathml.sml	Mon Jun 21 14:39:52 2021 +0200
     1.2 +++ b/test/Tools/isac/BridgeLibisabelle/mathml.sml	Mon Jun 21 15:36:09 2021 +0200
     1.3 @@ -49,15 +49,15 @@
     1.4  val t = @{term "aaa + bbb::real"};
     1.5  val ttt = HOLogic.mk_eq (t, Const ("processed_by_Isabelle_Isac", type_of t))
     1.6  (* check the term structure *)
     1.7 -val Const ("HOL.eq", T1) $
     1.8 -     (Const ("Groups.plus_class.plus", T2) $ 
     1.9 +val Const (\<^const_name>\<open>HOL.eq\<close>, T1) $
    1.10 +     (Const (\<^const_name>\<open>plus\<close>, T2) $ 
    1.11          Free ("aaa", T3) $ 
    1.12          Free ("bbb", _)) $
    1.13        Const ("processed_by_Isabelle_Isac", _) = ttt;
    1.14  
    1.15  (* check the type structure *)
    1.16  atomtyp T3;
    1.17 -Type ("Real.real", []);
    1.18 +Type (\<^type_name>\<open>real\<close>, []);
    1.19  
    1.20  atomtyp T2;
    1.21  (*
    1.22 @@ -69,11 +69,11 @@
    1.23  *** . . ]
    1.24  *** . ]
    1.25  with this \<up> build the typ ...*)
    1.26 -Type ("fun", [
    1.27 -  Type ("Real.real", []), 
    1.28 -  Type ("fun", [
    1.29 -    Type ("Real.real", []), 
    1.30 -    Type ("Real.real", [])])]);
    1.31 +Type (\<^type_name>\<open>fun\<close>, [
    1.32 +  Type (\<^type_name>\<open>real\<close>, []), 
    1.33 +  Type (\<^type_name>\<open>fun\<close>, [
    1.34 +    Type (\<^type_name>\<open>real\<close>, []), 
    1.35 +    Type (\<^type_name>\<open>real\<close>, [])])]);
    1.36  
    1.37  atomtyp T1;
    1.38  (*
    1.39 @@ -85,33 +85,33 @@
    1.40  *** . . ]
    1.41  *** . ]
    1.42  with this \<up> build the typ ...*)
    1.43 -Type ("fun", [
    1.44 -  Type ("Real.real", []), 
    1.45 -  Type ("fun", [
    1.46 -    Type ("Real.real", []), 
    1.47 -    Type ("HOL.bool", [])])]);
    1.48 +Type (\<^type_name>\<open>fun\<close>, [
    1.49 +  Type (\<^type_name>\<open>real\<close>, []), 
    1.50 +  Type (\<^type_name>\<open>fun\<close>, [
    1.51 +    Type (\<^type_name>\<open>real\<close>, []), 
    1.52 +    Type (\<^type_name>\<open>bool\<close>, [])])]);
    1.53  
    1.54  (* now compose term + typ *)
    1.55 -val Const ("HOL.eq", Type ("fun", [
    1.56 -                       Type ("Real.real", []), 
    1.57 -                       Type ("fun", [
    1.58 -                         Type ("Real.real", []), 
    1.59 -                         Type ("HOL.bool", [])])])) $
    1.60 -     (Const ("Groups.plus_class.plus", Type ("fun", [
    1.61 -                                         Type ("Real.real", []), 
    1.62 -                                         Type ("fun", [
    1.63 -                                           Type ("Real.real", []), 
    1.64 -                                           Type ("Real.real", [])])])) $ 
    1.65 -        Free ("aaa", Type ("Real.real", [])) $ 
    1.66 -        Free ("bbb", Type ("Real.real", []))) $
    1.67 -      Const ("processed_by_Isabelle_Isac", Type ("Real.real", [])) = ttt;
    1.68 +val Const (\<^const_name>\<open>HOL.eq\<close>, Type (\<^type_name>\<open>fun\<close>, [
    1.69 +                       Type (\<^type_name>\<open>real\<close>, []), 
    1.70 +                       Type (\<^type_name>\<open>fun\<close>, [
    1.71 +                         Type (\<^type_name>\<open>real\<close>, []), 
    1.72 +                         Type (\<^type_name>\<open>bool\<close>, [])])])) $
    1.73 +     (Const (\<^const_name>\<open>plus\<close>, Type (\<^type_name>\<open>fun\<close>, [
    1.74 +                                         Type (\<^type_name>\<open>real\<close>, []), 
    1.75 +                                         Type (\<^type_name>\<open>fun\<close>, [
    1.76 +                                           Type (\<^type_name>\<open>real\<close>, []), 
    1.77 +                                           Type (\<^type_name>\<open>real\<close>, [])])])) $ 
    1.78 +        Free ("aaa", Type (\<^type_name>\<open>real\<close>, [])) $ 
    1.79 +        Free ("bbb", Type (\<^type_name>\<open>real\<close>, []))) $
    1.80 +      Const ("processed_by_Isabelle_Isac", Type (\<^type_name>\<open>real\<close>, [])) = ttt;
    1.81  
    1.82  (* match out the original term from result*)
    1.83 -val Const ("HOL.eq", Type ("fun", [
    1.84 -                       Type ("Real.real", []), 
    1.85 -                       Type ("fun", [
    1.86 -                         Type ("Real.real", []), 
    1.87 -                         Type ("HOL.bool", [])])])) $
    1.88 +val Const (\<^const_name>\<open>HOL.eq\<close>, Type (\<^type_name>\<open>fun\<close>, [
    1.89 +                       Type (\<^type_name>\<open>real\<close>, []), 
    1.90 +                       Type (\<^type_name>\<open>fun\<close>, [
    1.91 +                         Type (\<^type_name>\<open>real\<close>, []), 
    1.92 +                         Type (\<^type_name>\<open>bool\<close>, [])])])) $
    1.93        t' $
    1.94 -      Const ("processed_by_Isabelle_Isac", Type ("Real.real", [])) = ttt;
    1.95 +      Const ("processed_by_Isabelle_Isac", Type (\<^type_name>\<open>real\<close>, [])) = ttt;
    1.96  if t = t' then () else error "something with test_term changed"