equal
deleted
inserted
replaced
39 fun check ctxt = |
39 fun check ctxt = |
40 #1 o Name_Space.check (Context.Proof ctxt) (Data.get (Proof_Context.theory_of ctxt)); |
40 #1 o Name_Space.check (Context.Proof ctxt) (Data.get (Proof_Context.theory_of ctxt)); |
41 |
41 |
42 val _ = Theory.setup |
42 val _ = Theory.setup |
43 (ML_Antiquotation.inline @{binding plugin} |
43 (ML_Antiquotation.inline @{binding plugin} |
44 (Args.context -- Scan.lift (Parse.position Args.name) |
44 (Args.context -- Scan.lift (Parse.position Args.embedded) |
45 >> (ML_Syntax.print_string o uncurry check))); |
45 >> (ML_Syntax.print_string o uncurry check))); |
46 |
46 |
47 |
47 |
48 (* indirections *) |
48 (* indirections *) |
49 |
49 |