1.1 --- a/src/Pure/Isar/spec_rules.ML	Sat Apr 16 15:25:25 2011 +0200
     1.2 +++ b/src/Pure/Isar/spec_rules.ML	Sat Apr 16 15:47:52 2011 +0200
     1.3 @@ -48,7 +48,7 @@
     1.4  
     1.5  fun add class (ts, ths) lthy =
     1.6    let
     1.7 -    val cts = map (Thm.cterm_of (ProofContext.theory_of lthy)) ts;
     1.8 +    val cts = map (Thm.cterm_of (Proof_Context.theory_of lthy)) ts;
     1.9    in
    1.10      lthy |> Local_Theory.declaration true
    1.11        (fn phi =>