changeset 34245 | 25bd3ed2ac9f |
parent 33701 | 9dd1079cec3a |
child 34259 | 2ba492b8b6e8 |
--- a/src/Pure/theory.ML Mon Jan 04 14:09:56 2010 +0100 +++ b/src/Pure/theory.ML Mon Jan 04 14:09:56 2010 +0100 @@ -91,7 +91,6 @@ type T = thy; val empty_axioms = Name_Space.empty_table "axiom" : term Name_Space.table; val empty = make_thy (empty_axioms, Defs.empty, ([], [])); - val copy = I; fun extend (Thy {axioms = _, defs, wrappers}) = make_thy (empty_axioms, defs, wrappers);