changeset 42360 | da8817d01e7c |
parent 41472 | f6ab14e61604 |
child 45291 | 57cd50f98fdc |
--- a/src/Pure/Isar/spec_rules.ML Sat Apr 16 15:25:25 2011 +0200 +++ b/src/Pure/Isar/spec_rules.ML Sat Apr 16 15:47:52 2011 +0200 @@ -48,7 +48,7 @@ fun add class (ts, ths) lthy = let - val cts = map (Thm.cterm_of (ProofContext.theory_of lthy)) ts; + val cts = map (Thm.cterm_of (Proof_Context.theory_of lthy)) ts; in lthy |> Local_Theory.declaration true (fn phi =>