equal
deleted
inserted
replaced
73 val get_stored_thm = hd o get_stored_thms; |
73 val get_stored_thm = hd o get_stored_thms; |
74 |
74 |
75 fun ml_store get (name, ths) = |
75 fun ml_store get (name, ths) = |
76 let |
76 let |
77 val ths' = Context.>>> (Context.map_theory_result |
77 val ths' = Context.>>> (Context.map_theory_result |
78 (PureThy.store_thms (Binding.name name, ths))); |
78 (Global_Theory.store_thms (Binding.name name, ths))); |
79 val _ = Context.>> (Context.map_theory (Stored_Thms.put ths')); |
79 val _ = Context.>> (Context.map_theory (Stored_Thms.put ths')); |
80 val _ = |
80 val _ = |
81 if name = "" then () |
81 if name = "" then () |
82 else if not (ML_Syntax.is_identifier name) then |
82 else if not (ML_Syntax.is_identifier name) then |
83 error ("Cannot bind theorem(s) " ^ quote name ^ " as ML value") |
83 error ("Cannot bind theorem(s) " ^ quote name ^ " as ML value") |