src/HOL/Tools/BNF/bnf_util.ML
changeset 59859 f9d1442c70f3
parent 59858 890b68e1e8b6
child 59860 a979fc5db526
--- a/src/HOL/Tools/BNF/bnf_util.ML	Mon Mar 30 22:34:59 2015 +0200
+++ b/src/HOL/Tools/BNF/bnf_util.ML	Tue Mar 31 00:11:54 2015 +0200
@@ -145,7 +145,7 @@
     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.conceal
+      |> Local_Theory.concealed
       |> Typedef.add_typedef true (b', Ts, mx) set opt_morphs tac
       ||> Local_Theory.restore_naming lthy
       ||> `Local_Theory.restore;