src/Pure/simplifier.ML

       {name = Local_Theory.full_name lthy b,
        lhss =
         let
           val lhss' = prep lthy lhss;
           val ctxt' = fold Variable.auto_fixes lhss' lthy;
-        in Variable.export_terms ctxt' lthy lhss' end |> map (Proof_Context.cterm_of lthy),
+        in Variable.export_terms ctxt' lthy lhss' end |> map (Thm.cterm_of lthy),
        proc = proc,
        identifier = identifier};
   in
     lthy |> Local_Theory.declaration {syntax = false, pervasive = true} (fn phi => fn context =>
       let