--- a/src/HOL/Tools/BNF/bnf_util.ML Tue Mar 31 16:47:12 2015 +0200
+++ b/src/HOL/Tools/BNF/bnf_util.ML Tue Mar 31 17:34:52 2015 +0200
@@ -145,9 +145,9 @@
val b' = fold_rev Binding.prefix_name (map (suffix "_" o fst) (Binding.path_of b)) b;
val ((name, info), (lthy, lthy_old)) =
lthy
- |> Local_Theory.concealed
+ |> Proof_Context.concealed
|> Typedef.add_typedef true (b', Ts, mx) set opt_morphs tac
- ||> Local_Theory.restore_naming lthy
+ ||> Proof_Context.restore_naming lthy
||> `Local_Theory.restore;
val phi = Proof_Context.export_morphism lthy_old lthy;
in