changeset 70454 | fa933b98d64d |
parent 70451 | 550a5a822edb |
child 70458 | 9e2173eb23eb |
--- a/src/Pure/proofterm.ML Thu Aug 01 09:55:37 2019 +0200 +++ b/src/Pure/proofterm.ML Thu Aug 01 10:14:58 2019 +0200 @@ -2064,6 +2064,11 @@ fun prepare_thm_proof unconstrain thy name shyps hyps concl promises body = let +(* + val FIXME = + Output.physical_stderr ("pthm " ^ quote name ^ " " ^ Position.here (Position.thread_data ()) ^ "\n"); +*) + val named = name <> ""; val prop = Logic.list_implies (hyps, concl);