src/HOL/Tools/BNF/bnf_lift.ML
changeset 69593 3dda49e08b9d
parent 67091 1393c2340eec
     1.1 --- a/src/HOL/Tools/BNF/bnf_lift.ML	Fri Jan 04 21:49:06 2019 +0100
     1.2 +++ b/src/HOL/Tools/BNF/bnf_lift.ML	Fri Jan 04 23:22:53 2019 +0100
     1.3 @@ -357,11 +357,11 @@
     1.4        | NONE => Typedef.get_info lthy Tname |> hd |> snd |> #type_definition);
     1.5      val wits = (Option.map o map) (prepare_term lthy) raw_wits;
     1.6      val specs =
     1.7 -      map (apsnd (apsnd (the_default @{sort type} o Option.map (prepare_sort lthy)))) raw_specs;
     1.8 +      map (apsnd (apsnd (the_default \<^sort>\<open>type\<close> o Option.map (prepare_sort lthy)))) raw_specs;
     1.9  
    1.10      val _ =
    1.11        (case HOLogic.dest_Trueprop (Thm.prop_of input_thm) of
    1.12 -        Const (@{const_name type_definition}, _) $ _ $ _ $ _ => ()
    1.13 +        Const (\<^const_name>\<open>type_definition\<close>, _) $ _ $ _ $ _ => ()
    1.14        | _ => error "Unsupported type of a theorem: only type_definition is supported");
    1.15    in
    1.16      typedef_bnf input_thm wits specs map_b rel_b pred_b plugins lthy
    1.17 @@ -415,20 +415,20 @@
    1.18  local
    1.19  
    1.20  val parse_wits =
    1.21 -  @{keyword "["} |-- (Parse.name --| @{keyword ":"} -- Scan.repeat Parse.term >>
    1.22 +  \<^keyword>\<open>[\<close> |-- (Parse.name --| \<^keyword>\<open>:\<close> -- Scan.repeat Parse.term >>
    1.23      (fn ("wits", Ts) => Ts
    1.24        | (s, _) => error ("Unknown label " ^ quote s ^ " (expected \"wits\")"))) --|
    1.25 -  @{keyword "]"} || Scan.succeed [];
    1.26 +  \<^keyword>\<open>]\<close> || Scan.succeed [];
    1.27  
    1.28  val parse_options =
    1.29 -  Scan.optional (@{keyword "("} |--
    1.30 +  Scan.optional (\<^keyword>\<open>(\<close> |--
    1.31      Parse.list1 (Parse.group (K "option")
    1.32        (Plugin_Name.parse_filter >> Plugins_Option
    1.33        || Parse.reserved "no_warn_wits" >> K No_Warn_Wits))
    1.34 -    --| @{keyword ")"}) [];
    1.35 +    --| \<^keyword>\<open>)\<close>) [];
    1.36  
    1.37  val parse_plugins =
    1.38 -  Scan.optional (@{keyword "("} |-- Plugin_Name.parse_filter --| @{keyword ")"})
    1.39 +  Scan.optional (\<^keyword>\<open>(\<close> |-- Plugin_Name.parse_filter --| \<^keyword>\<open>)\<close>)
    1.40      (K Plugin_Name.default_filter) >> Plugins_Option >> single;
    1.41  
    1.42  val parse_typedef_thm = Scan.option (Parse.reserved "via" |-- Parse.thm);
    1.43 @@ -436,13 +436,13 @@
    1.44  in
    1.45  
    1.46  val _ =
    1.47 -  Outer_Syntax.local_theory_to_proof @{command_keyword lift_bnf}
    1.48 +  Outer_Syntax.local_theory_to_proof \<^command_keyword>\<open>lift_bnf\<close>
    1.49      "register a subtype of a bounded natural functor (BNF) as a BNF"
    1.50      ((parse_options -- parse_type_args_named_constrained -- Parse.type_const -- parse_wits --
    1.51        parse_typedef_thm -- parse_map_rel_pred_bindings) >> lift_bnf_cmd);
    1.52  
    1.53  val _ =
    1.54 -  Outer_Syntax.local_theory @{command_keyword copy_bnf}
    1.55 +  Outer_Syntax.local_theory \<^command_keyword>\<open>copy_bnf\<close>
    1.56      "register a type copy of a bounded natural functor (BNF) as a BNF"
    1.57      ((parse_plugins -- parse_type_args_named_constrained -- Parse.type_const --
    1.58        parse_typedef_thm -- parse_map_rel_pred_bindings) >> copy_bnf_cmd);