equal
deleted
inserted
replaced
598 (case Proof_Context.read_const {proper = false, strict = false} ctxt c of |
598 (case Proof_Context.read_const {proper = false, strict = false} ctxt c of |
599 Free (x, _) => |
599 Free (x, _) => |
600 let |
600 let |
601 val ctxt' = |
601 val ctxt' = |
602 ctxt |> is_none (Variable.default_type ctxt x) ? |
602 ctxt |> is_none (Variable.default_type ctxt x) ? |
603 Variable.declare_constraints (Free (x, Mixfix.mixfixT mx)); |
603 Variable.declare_constraints (Free (x, Proof_Context.default_constraint ctxt mx)); |
604 val t = Free (#1 (Proof_Context.inferred_param x ctxt')); |
604 val t = Free (#1 (Proof_Context.inferred_param x ctxt')); |
605 in ((t, mx), ctxt') end |
605 in ((t, mx), ctxt') end |
606 | t => ((t, mx), ctxt)); |
606 | t => ((t, mx), ctxt)); |
607 |
607 |
608 fun gen_write prep_arg mode args = |
608 fun gen_write prep_arg mode args = |