src/HOL/Library/simps_case_conv.ML

 
 fun import [] ctxt = ([], ctxt)
   | import (thm :: thms) ctxt =
     let
       val fun_ct = strip_eq #> fst #> strip_comb #> fst #> Logic.mk_term
-        #> Proof_Context.cterm_of ctxt
+        #> Thm.cterm_of ctxt
       val ct = fun_ct thm
       val cts = map fun_ct thms
       val pairs = map (fn s => (s,ct)) cts
       val thms' = map (fn (th,p) => Thm.instantiate (Thm.match p) th) (thms ~~ pairs)
     in Variable.import true (thm :: thms') ctxt |> apfst snd end