src/HOL/Types_To_Sets/local_typedef.ML
changeset 69597 ff784d5a5bfb
parent 64551 79e9587dbcca
     1.1 --- a/src/HOL/Types_To_Sets/local_typedef.ML	Sat Jan 05 17:00:43 2019 +0100
     1.2 +++ b/src/HOL/Types_To_Sets/local_typedef.ML	Sat Jan 05 17:24:33 2019 +0100
     1.3 @@ -23,9 +23,9 @@
     1.4  
     1.5  (** BEGINNING OF THE CRITICAL CODE **)
     1.6  
     1.7 -fun dest_typedef (Const (@{const_name Ex}, _) $ Abs (_, _,
     1.8 -      (Const (@{const_name Ex}, _) $ Abs (_, Abs_type,
     1.9 -      (Const (@{const_name type_definition}, _)) $ Bound 1 $ Bound 0 $ set)))) =
    1.10 +fun dest_typedef (Const (\<^const_name>\<open>Ex\<close>, _) $ Abs (_, _,
    1.11 +      (Const (\<^const_name>\<open>Ex\<close>, _) $ Abs (_, Abs_type,
    1.12 +      (Const (\<^const_name>\<open>type_definition\<close>, _)) $ Bound 1 $ Bound 0 $ set)))) =
    1.13      (Abs_type, set)
    1.14     | dest_typedef t = raise TERM ("dest_typedef", [t]);
    1.15  
    1.16 @@ -71,14 +71,14 @@
    1.17  (** END OF THE CRITICAL CODE **)
    1.18  
    1.19  val (_, cancel_type_definition_oracle) = Context.>>> (Context.map_theory_result
    1.20 -  (Thm.add_oracle (@{binding cancel_type_definition}, cancel_type_definition_cterm)));
    1.21 +  (Thm.add_oracle (\<^binding>\<open>cancel_type_definition\<close>, cancel_type_definition_cterm)));
    1.22  
    1.23  fun cancel_type_definition thm =
    1.24    Drule.implies_elim_list (cancel_type_definition_oracle thm) (map Thm.assume (Thm.chyps_of thm));
    1.25  
    1.26  val cancel_type_definition_attr = Thm.rule_attribute [] (K cancel_type_definition);
    1.27  
    1.28 -val _ = Context.>> (Context.map_theory (Attrib.setup @{binding cancel_type_definition}
    1.29 +val _ = Context.>> (Context.map_theory (Attrib.setup \<^binding>\<open>cancel_type_definition\<close>
    1.30    (Scan.succeed cancel_type_definition_attr) "cancel a local type definition"));
    1.31  
    1.32  end;