555 fun parseNEW' ctxt str = |
555 fun parseNEW' ctxt str = |
556 case parseNEW ctxt str of |
556 case parseNEW ctxt str of |
557 SOME t => t |
557 SOME t => t |
558 | NONE => raise TERM ("NO parseNEW' for " ^ str, []) |
558 | NONE => raise TERM ("NO parseNEW' for " ^ str, []) |
559 fun parseNEW'' thy str = |
559 fun parseNEW'' thy str = |
560 case parseNEW (ThyC.to_ctxt thy) str of |
560 case parseNEW (Proof_Context.init_global thy) str of |
561 SOME t => t |
561 SOME t => t |
562 | NONE => raise TERM ("NO parseNEW'' for " ^ str, []) |
562 | NONE => raise TERM ("NO parseNEW'' for " ^ str, []) |
563 |
563 |
564 (* parse term patterns; Var ("v",_), i.e. "?v", are required for instantiation |
564 (* parse term patterns; Var ("v",_), i.e. "?v", are required for instantiation |
565 WN130613 probably compare to |
565 WN130613 probably compare to |
566 http://www.mail-archive.com/isabelle-dev@mailbroy.informatik.tu-muenchen.de/msg04249.html*) |
566 http://www.mail-archive.com/isabelle-dev@mailbroy.informatik.tu-muenchen.de/msg04249.html*) |
567 fun parse_patt thy str = (thy, str) |
567 fun parse_patt thy str = (thy, str) |
568 |>> ThyC.to_ctxt |
568 |>> Proof_Context.init_global |
569 |-> Proof_Context.read_term_pattern |
569 |-> Proof_Context.read_term_pattern |
570 (*|> numbers_to_string TODO drop*) |
570 (*|> numbers_to_string TODO drop*) |
571 |> typ_a2real; (*TODO drop*) |
571 |> typ_a2real; (*TODO drop*) |
572 fun str2term str = parse_patt (ThyC.get_theory "Isac_Knowledge") str |
572 fun str2term str = parse_patt (ThyC.get_theory "Isac_Knowledge") str |
573 |
573 |