diff -r 92d7d8e4f1bf -r 291934bac95e src/Pure/Isar/spec_rules.ML
--- a/src/Pure/Isar/spec_rules.ML	Fri Mar 06 14:01:08 2015 +0100
+++ b/src/Pure/Isar/spec_rules.ML	Fri Mar 06 15:58:56 2015 +0100
@@ -48,7 +48,7 @@
 
 fun add class (ts, ths) lthy =
   let
-    val cts = map (Proof_Context.cterm_of lthy) ts;
+    val cts = map (Thm.cterm_of lthy) ts;
   in
     lthy |> Local_Theory.declaration {syntax = false, pervasive = true}
       (fn phi =>