# 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)));