--- a/src/HOL/Tools/BNF/bnf_lfp_countable.ML Sat Jan 05 17:00:43 2019 +0100
+++ b/src/HOL/Tools/BNF/bnf_lfp_countable.ML Sat Jan 05 17:24:33 2019 +0100
@@ -70,13 +70,13 @@
fun encode_sumN n k t =
Balanced_Tree.access {init = t,
- left = fn t => @{const sum_encode} $ (@{const Inl (nat, nat)} $ t),
- right = fn t => @{const sum_encode} $ (@{const Inr (nat, nat)} $ t)}
+ left = fn t => \<^const>\<open>sum_encode\<close> $ (@{const Inl (nat, nat)} $ t),
+ right = fn t => \<^const>\<open>sum_encode\<close> $ (@{const Inr (nat, nat)} $ t)}
n k;
fun encode_tuple [] = \<^term>\<open>0 :: nat\<close>
| encode_tuple ts =
- Balanced_Tree.make (fn (t, u) => @{const prod_encode} $ (@{const Pair (nat, nat)} $ u $ t)) ts;
+ Balanced_Tree.make (fn (t, u) => \<^const>\<open>prod_encode\<close> $ (@{const Pair (nat, nat)} $ u $ t)) ts;
fun mk_encode_funs ctxt fpTs ns ctrss0 recs0 =
let
@@ -181,7 +181,7 @@
|> map Thm.close_derivation
end;
-fun get_countable_goal_type_name (@{const Trueprop} $ (Const (\<^const_name>\<open>Ex\<close>, _)
+fun get_countable_goal_type_name (\<^const>\<open>Trueprop\<close> $ (Const (\<^const_name>\<open>Ex\<close>, _)
$ Abs (_, Type (_, [Type (s, _), _]), Const (\<^const_name>\<open>inj_on\<close>, _) $ Bound 0
$ Const (\<^const_name>\<open>top\<close>, _)))) = s
| get_countable_goal_type_name _ = error "Wrong goal format for datatype countability tactic";