| changeset 28820 | 95dd21624c6c |
| parent 28791 | cc16be808796 |
| child 28858 | 855e61829e22 |
--- a/src/Pure/Isar/specification.ML Mon Nov 17 17:00:21 2008 +0100 +++ b/src/Pure/Isar/specification.ML Mon Nov 17 17:00:22 2008 +0100 @@ -368,7 +368,7 @@ in val theorem = gen_theorem (K I) Locale.cert_context_statement; -val theorem_cmd = gen_theorem Attrib.intern_src Locale.read_context_statement_i; +val theorem_cmd = gen_theorem Attrib.intern_src Locale.read_context_statement; fun add_theorem_hook f = TheoremHook.map (cons (f, stamp ()));