src/HOL/Library/Countable.thy
changeset 69593 3dda49e08b9d
parent 68502 a8ada04583e7
child 69605 a96320074298
     1.1 --- a/src/HOL/Library/Countable.thy	Fri Jan 04 21:49:06 2019 +0100
     1.2 +++ b/src/HOL/Library/Countable.thy	Fri Jan 04 23:22:53 2019 +0100
     1.3 @@ -168,7 +168,7 @@
     1.4        let
     1.5          val ty_name =
     1.6            (case goal of
     1.7 -            (_ $ Const (@{const_name Pure.type}, Type (@{type_name itself}, [Type (n, _)]))) => n
     1.8 +            (_ $ Const (\<^const_name>\<open>Pure.type\<close>, Type (\<^type_name>\<open>itself\<close>, [Type (n, _)]))) => n
     1.9            | _ => raise Match)
    1.10          val typedef_info = hd (Typedef.get_info ctxt ty_name)
    1.11          val typedef_thm = #type_definition (snd typedef_info)
    1.12 @@ -183,7 +183,7 @@
    1.13          val induct_thm = the (AList.lookup (op =) alist pred_name)
    1.14          val vars = rev (Term.add_vars (Thm.prop_of induct_thm) [])
    1.15          val insts = vars |> map (fn (_, T) => try (Thm.cterm_of ctxt)
    1.16 -          (Const (@{const_name Countable.finite_item}, T)))
    1.17 +          (Const (\<^const_name>\<open>Countable.finite_item\<close>, T)))
    1.18          val induct_thm' = Thm.instantiate' [] insts induct_thm
    1.19          val rules = @{thms finite_item.intros}
    1.20        in