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;