| changeset 33457 | 0fc03a81c27c |
| parent 33454 | 485fd398dd33 |
| child 33519 | e31a85f92ce9 |
--- a/src/Pure/Isar/spec_rules.ML Thu Nov 05 22:06:46 2009 +0100 +++ b/src/Pure/Isar/spec_rules.ML Thu Nov 05 22:08:47 2009 +0100 @@ -41,7 +41,7 @@ val get = Item_Net.content o Rules.get o Context.Proof; val get_global = Item_Net.content o Rules.get o Context.Theory; -fun add class (ts, ths) = LocalTheory.declaration +fun add class (ts, ths) = LocalTheory.declaration true (fn phi => let val ts' = map (Morphism.term phi) ts;