1.1 --- a/test/Tools/isac/BridgeLibisabelle/mathml.sml	Mon Apr 19 11:45:43 2021 +0200
     1.2 +++ b/test/Tools/isac/BridgeLibisabelle/mathml.sml	Mon Apr 19 15:02:00 2021 +0200
     1.3 @@ -42,24 +42,24 @@
     1.4  
     1.5  (*========== inhibit exn AK110725 ================================================
     1.6  "----- check 'manually' the xml-output of calling functions ------";
     1.7 -formula2xml 1 (str2term str);
     1.8 +formula2xml 1 (TermC.str2term str);
     1.9  
    1.10  (* AK110725 
    1.11 -(*str2term str; (* ERROR: Inner syntax error at "; 0 < ?n |] ==> ?a / ?b ^ ?n = ?a * ?b ^ - ?n"
    1.12 -                   Failed to parse term*)*)
    1.13 -"~~~~~ fun str2term, args:"; val (str) = (str);
    1.14 +(*TermC.str2term str; (* ERROR: Inner syntax error at "; 0 < ?n |] ==> ?a / ?b ^ ?n = ?a * ?b ^ - ?n"
    1.15 +                   Failed to TermC.parse term*)*)
    1.16 +"~~~~~ fun TermC.str2term, args:"; val (str) = (str);
    1.17  ThyC.get_theory "Isac_Knowledge";
    1.18  
    1.19 -parse_patt;
    1.20 -parse_patt (ThyC.get_theory "Isac_Knowledge");
    1.21 -(*parse_patt (ThyC.get_theory "Isac_Knowledge") str; (* ERROR: Inner syntax error at "; 0 < ?n |] ==> ?a / ?b ^ ?n = ?a * ?b ^ - ?n"
    1.22 -Failed to parse term*)*)
    1.23 +TermC.parse_patt;
    1.24 +TermC.parse_patt (ThyC.get_theory "Isac_Knowledge");
    1.25 +(*TermC.parse_patt (ThyC.get_theory "Isac_Knowledge") str; (* ERROR: Inner syntax error at "; 0 < ?n |] ==> ?a / ?b ^ ?n = ?a * ?b ^ - ?n"
    1.26 +Failed to TermC.parse term*)*)
    1.27  
    1.28 -"~~~~~ fun parse_patt, args:"; val (thy, str) = ((ThyC.get_theory "Isac_Knowledge"), str);
    1.29 +"~~~~~ fun TermC.parse_patt, args:"; val (thy, str) = ((ThyC.get_theory "Isac_Knowledge"), str);
    1.30  (thy, str) 
    1.31  |>> ThyC.to_ctxt
    1.32  (*|-> Proof_Context.read_term_pattern (*ERROR: Inner syntax error at "; 0 < ?n |] ==> ?a / ?b ^ ?n = ?a * ?b ^ - ?n"
    1.33 -Failed to parse term*)*)
    1.34 +Failed to TermC.parse term*)*)
    1.35  
    1.36  Proof_Context.read_term_pattern;
    1.37  (@{theory "Isac_Knowledge"}, str) |>> ThyC.to_ctxt;