changeset 21440 | 807a39221a58 |
parent 20893 | c99f79910ae8 |
child 21483 | e4be91feca50 |
--- a/src/Pure/Tools/invoke.ML Tue Nov 21 18:07:36 2006 +0100 +++ b/src/Pure/Tools/invoke.ML Tue Nov 21 18:07:37 2006 +0100 @@ -80,7 +80,7 @@ ctxt |> ProofContext.sticky_prefix prfx |> ProofContext.qualified_names - |> (snd o ProofContext.note_thmss_i notes) + |> (snd o ProofContext.note_thmss_i "" notes) |> ProofContext.restore_naming ctxt end) #> Proof.put_facts NONE #> Seq.single;