1.1 --- a/test/Tools/isac/BridgeLibisabelle/mathml.sml	Wed Apr 15 11:37:43 2020 +0200
     1.2 +++ b/test/Tools/isac/BridgeLibisabelle/mathml.sml	Wed Apr 15 13:47:56 2020 +0200
     1.3 @@ -48,21 +48,21 @@
     1.4  (*str2term str; (* ERROR: Inner syntax error at "; 0 < ?n |] ==> ?a / ?b ^ ?n = ?a * ?b ^ - ?n"
     1.5                     Failed to parse term*)*)
     1.6  "~~~~~ fun str2term, args:"; val (str) = (str);
     1.7 -Thy_Info_get_theory "Isac_Knowledge";
     1.8 +ThyC.get_theory "Isac_Knowledge";
     1.9  
    1.10  parse_patt;
    1.11 -parse_patt (Thy_Info_get_theory "Isac_Knowledge");
    1.12 -(*parse_patt (Thy_Info_get_theory "Isac_Knowledge") str; (* ERROR: Inner syntax error at "; 0 < ?n |] ==> ?a / ?b ^ ?n = ?a * ?b ^ - ?n"
    1.13 +parse_patt (ThyC.get_theory "Isac_Knowledge");
    1.14 +(*parse_patt (ThyC.get_theory "Isac_Knowledge") str; (* ERROR: Inner syntax error at "; 0 < ?n |] ==> ?a / ?b ^ ?n = ?a * ?b ^ - ?n"
    1.15  Failed to parse term*)*)
    1.16  
    1.17 -"~~~~~ fun parse_patt, args:"; val (thy, str) = ((Thy_Info_get_theory "Isac_Knowledge"), str);
    1.18 +"~~~~~ fun parse_patt, args:"; val (thy, str) = ((ThyC.get_theory "Isac_Knowledge"), str);
    1.19  (thy, str) 
    1.20 -|>> thy2ctxt
    1.21 +|>> ThyC.to_ctxt
    1.22  (*|-> Proof_Context.read_term_pattern (*ERROR: Inner syntax error at "; 0 < ?n |] ==> ?a / ?b ^ ?n = ?a * ?b ^ - ?n"
    1.23  Failed to parse term*)*)
    1.24  
    1.25  Proof_Context.read_term_pattern;
    1.26 -(@{theory "Isac_Knowledge"}, str) |>> thy2ctxt;
    1.27 +(@{theory "Isac_Knowledge"}, str) |>> ThyC.to_ctxt;
    1.28  "~~~~~ fun Proof_Context.read_term_pattern, args:"; val () = ();
    1.29  (*AK110725 To be continued...*)
    1.30  *)