changeset 56002 | 2028467b4df4 |
parent 55997 | 9dc5ce83202c |
child 56897 | c668735fb8b5 |
--- a/src/Pure/Isar/proof.ML Sun Mar 09 15:21:08 2014 +0100 +++ b/src/Pure/Isar/proof.ML Sun Mar 09 16:37:56 2014 +0100 @@ -575,7 +575,7 @@ #> reset_facts; fun read_arg ctxt (c, mx) = - (case Proof_Context.read_const ctxt {proper = false, strict = false} c of + (case Proof_Context.read_const {proper = false, strict = false} ctxt c of Free (x, _) => let val T = Proof_Context.infer_type ctxt (x, Mixfix.mixfixT mx) in (Free (x, T), mx) end