equal
deleted
inserted
replaced
860 for the antiquotation @{text "term_pat"} is as follows. |
860 for the antiquotation @{text "term_pat"} is as follows. |
861 *} |
861 *} |
862 |
862 |
863 ML %linenosgray{*val term_pat_setup = |
863 ML %linenosgray{*val term_pat_setup = |
864 let |
864 let |
865 val parser = Args.context -- Scan.lift Args.name_source |
865 val parser = Args.context -- Scan.lift Args.name_inner_syntax |
866 |
866 |
867 fun term_pat (ctxt, str) = |
867 fun term_pat (ctxt, str) = |
868 str |> Proof_Context.read_term_pattern ctxt |
868 str |> Proof_Context.read_term_pattern ctxt |
869 |> ML_Syntax.print_term |
869 |> ML_Syntax.print_term |
870 |> ML_Syntax.atomic |
870 |> ML_Syntax.atomic |
893 we can write an antiquotation for type patterns. Its code is |
893 we can write an antiquotation for type patterns. Its code is |
894 *} |
894 *} |
895 |
895 |
896 ML %grayML{*val type_pat_setup = |
896 ML %grayML{*val type_pat_setup = |
897 let |
897 let |
898 val parser = Args.context -- Scan.lift Args.name_source |
898 val parser = Args.context -- Scan.lift Args.name_inner_syntax |
899 |
899 |
900 fun typ_pat (ctxt, str) = |
900 fun typ_pat (ctxt, str) = |
901 let |
901 let |
902 val ctxt' = Proof_Context.set_mode Proof_Context.mode_schematic ctxt |
902 val ctxt' = Proof_Context.set_mode Proof_Context.mode_schematic ctxt |
903 in |
903 in |