equal
deleted
inserted
replaced
936 ML{*val type_pat_setup = |
936 ML{*val type_pat_setup = |
937 let |
937 let |
938 val parser = Args.context -- Scan.lift Args.name_source |
938 val parser = Args.context -- Scan.lift Args.name_source |
939 |
939 |
940 fun typ_pat (ctxt, str) = |
940 fun typ_pat (ctxt, str) = |
941 str |> Syntax.parse_typ ctxt |
941 let |
942 |> ML_Syntax.print_typ |
942 val ctxt' = Proof_Context.set_mode Proof_Context.mode_schematic ctxt |
943 |> ML_Syntax.atomic |
943 in |
|
944 str |> Syntax.read_typ ctxt' |
|
945 |> ML_Syntax.print_typ |
|
946 |> ML_Syntax.atomic |
|
947 end |
944 in |
948 in |
945 ML_Antiquote.inline @{binding "typ_pat"} (parser >> typ_pat) |
949 ML_Antiquote.inline @{binding "typ_pat"} (parser >> typ_pat) |
946 end*} |
950 end*} |
947 |
951 |
948 text {* |
952 text {* |