changeset 67715 | ec46ecb87999 |
parent 67147 | dea94b1aabc3 |
child 70494 | 41108e3e9ca5 |
--- a/src/Pure/ML/ml_thms.ML Fri Feb 23 21:12:08 2018 +0100 +++ b/src/Pure/ML/ml_thms.ML Fri Feb 23 21:27:20 2018 +0100 @@ -120,8 +120,9 @@ fun ml_store get (name, ths) = let - val ths' = Context.>>> (Context.map_theory_result - (Global_Theory.store_thms (Binding.name name, ths))); + val (_, ths') = + Context.>>> (Context.map_theory_result + (Global_Theory.note_thms "" ((Binding.name name, []), [(ths, [])]))); val _ = Theory.setup (Stored_Thms.put ths'); val _ = if name = "" then ()