# HG changeset patch # User wenzelm # Date 1258314994 -3600 # Node ID 9e6b6594da6bad55c03592e6cf98c3c73d5b1aaa # Parent 9dd1079cec3a94fd6eabcf2ca8ff963131887891 use simultaneous Morphics.fact; diff -r 9dd1079cec3a -r 9e6b6594da6b src/Pure/Isar/spec_rules.ML --- a/src/Pure/Isar/spec_rules.ML Sun Nov 15 20:39:22 2009 +0100 +++ b/src/Pure/Isar/spec_rules.ML Sun Nov 15 20:56:34 2009 +0100 @@ -41,12 +41,19 @@ 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) = Local_Theory.declaration true - (fn phi => - let - val ts' = map (Morphism.term phi) ts; - val ths' = map (Morphism.thm phi) ths; - in Rules.map (Item_Net.update (class, (ts', ths'))) end); +fun add class (ts, ths) lthy = + let + val cts = map (Thm.cterm_of (ProofContext.theory_of lthy)) ts; + in + lthy |> Local_Theory.declaration true + (fn phi => + let + val (ts', ths') = + Morphism.fact phi (map Drule.mk_term cts @ ths) + |> chop (length cts) + |>> map (Thm.term_of o Drule.dest_term); + in Rules.map (Item_Net.update (class, (ts', ths'))) end) + end; fun add_global class spec = Context.theory_map (Rules.map (Item_Net.update (class, spec)));