src/Pure/Isar/proof.ML
changeset 62771 dd2914250ca7
parent 62663 bea354f6ff21
child 62773 e6443edaebff
equal deleted inserted replaced
62770:6e6cacf8fe50 62771:dd2914250ca7
   592 
   592 
   593 (* concrete syntax *)
   593 (* concrete syntax *)
   594 
   594 
   595 local
   595 local
   596 
   596 
       
   597 fun read_arg (c, mx) ctxt =
       
   598   (case Proof_Context.read_const {proper = false, strict = false} ctxt c of
       
   599     Free (x, _) =>
       
   600       let
       
   601         val ctxt' =
       
   602           ctxt |> is_none (Variable.default_type ctxt x) ?
       
   603             Variable.declare_constraints (Free (x, Mixfix.mixfixT mx));
       
   604         val t = Free (#1 (Proof_Context.inferred_param x ctxt'));
       
   605       in ((t, mx), ctxt') end
       
   606   | t => ((t, mx), ctxt));
       
   607 
   597 fun gen_write prep_arg mode args =
   608 fun gen_write prep_arg mode args =
   598   assert_forward
   609   assert_forward
   599   #> map_context (fn ctxt => ctxt |> Proof_Context.notation true mode (map (prep_arg ctxt) args))
   610   #> map_context (fold_map prep_arg args #-> Proof_Context.notation true mode)
   600   #> reset_facts;
   611   #> reset_facts;
   601 
   612 
   602 fun read_arg ctxt (c, mx) =
   613 in
   603   (case Proof_Context.read_const {proper = false, strict = false} ctxt c of
   614 
   604     Free (x, _) =>
   615 val write = gen_write pair;
   605       let val T = Proof_Context.infer_type ctxt (x, Mixfix.mixfixT mx)
       
   606       in (Free (x, T), mx) end
       
   607   | t => (t, mx));
       
   608 
       
   609 in
       
   610 
       
   611 val write = gen_write (K I);
       
   612 val write_cmd = gen_write read_arg;
   616 val write_cmd = gen_write read_arg;
   613 
   617 
   614 end;
   618 end;
   615 
   619 
   616 
   620