55 Failed to parse term*)*) |
55 Failed to parse term*)*) |
56 |
56 |
57 "~~~~~ fun parse_patt, args:"; val (thy, str) = ((Thy_Info.get_theory "Isac"), str); |
57 "~~~~~ fun parse_patt, args:"; val (thy, str) = ((Thy_Info.get_theory "Isac"), str); |
58 (thy, str) |
58 (thy, str) |
59 |>> thy2ctxt |
59 |>> thy2ctxt |
60 (*|-> ProofContext.read_term_pattern (*ERROR: Inner syntax error at "; 0 < ?n |] ==> ?a / ?b ^ ?n = ?a * ?b ^ - ?n" |
60 (*|-> Proof_Context.read_term_pattern (*ERROR: Inner syntax error at "; 0 < ?n |] ==> ?a / ?b ^ ?n = ?a * ?b ^ - ?n" |
61 Failed to parse term*)*) |
61 Failed to parse term*)*) |
62 |
62 |
63 ProofContext.read_term_pattern; |
63 Proof_Context.read_term_pattern; |
64 (@{theory "Isac"}, str) |>> thy2ctxt; |
64 (@{theory "Isac"}, str) |>> thy2ctxt; |
65 "~~~~~ fun ProofContext.read_term_pattern, args:"; val () = (); |
65 "~~~~~ fun Proof_Context.read_term_pattern, args:"; val () = (); |
66 (*AK110725 To be continued...*) |
66 (*AK110725 To be continued...*) |
67 *) |
67 *) |
68 (*==================================================================*) |
68 (*==================================================================*) |
69 "-----------------------------------------------------------------"; |
69 "-----------------------------------------------------------------"; |
70 "exported from struct --------------------------------------------"; |
70 "exported from struct --------------------------------------------"; |