src/HOL/thy_syntax.ML
changeset 14598 7009f59711e3
parent 12505 46bfc675015a
child 14672 79bac83b2c27
     1.1 --- a/src/HOL/thy_syntax.ML	Fri Apr 16 18:44:39 2004 +0200
     1.2 +++ b/src/HOL/thy_syntax.ML	Fri Apr 16 18:45:56 2004 +0200
     1.3 @@ -57,7 +57,7 @@
     1.4      fun mk_params ((recs, ipairs), monos) =
     1.5        let val big_rec_name = space_implode "_" (map (scan_to_id o unenclose) recs)
     1.6            and srec_tms = mk_list recs
     1.7 -          and sintrs   = mk_big_list (no_atts (map (mk_pair o apfst quote) ipairs))
     1.8 +          and sintrs   = mk_big_list (no_atts (map (mk_pair o apfst Library.quote) ipairs))
     1.9        in
    1.10          ";\n\n\
    1.11          \local\n\
    1.12 @@ -133,7 +133,7 @@
    1.13        val names = map (fn ((((alt_name, _), name), _), _) =>
    1.14          unenclose (if_none alt_name name)) dts;
    1.15  
    1.16 -      val add_datatype_args = brackets (commas (map quote names)) ^ " " ^
    1.17 +      val add_datatype_args = brackets (commas (map Library.quote names)) ^ " " ^
    1.18          brackets (commas (map (fn ((((_, vs), name), mx), cs) =>
    1.19            parens (brackets (commas vs) ^ ", " ^ name ^ ", " ^ mx ^ ", " ^
    1.20              brackets (commas cs))) dts));
    1.21 @@ -156,7 +156,7 @@
    1.22      \  case_thms, split_thms, induction, size, simps}) =\n\
    1.23      \ DatatypePackage.rep_datatype " ^
    1.24      (case names of
    1.25 -        Some names => "(Some [" ^ commas_quote names ^ "])\n " ^
    1.26 +        Some names => "(Some [" ^ Library.commas_quote names ^ "])\n " ^
    1.27            mk_thmss distinct ^ "\n " ^ mk_thmss inject ^
    1.28              "\n " ^ mk_thm induct ^ " thy;\nin\n" ^ mk_bind_thms_string names
    1.29        | None => "None\n " ^ mk_thmss distinct ^ "\n " ^ mk_thmss inject ^
    1.30 @@ -179,7 +179,7 @@
    1.31    val opt_typs = repeat ((string >> unenclose) ||
    1.32      simple_typ || ("(" $$-- complex_typ --$$ ")"));
    1.33    val constructor = name -- opt_typs -- opt_mixfix >> (fn ((n, Ts), mx) =>
    1.34 -    parens (n ^ ", " ^ brackets (commas_quote Ts) ^ ", " ^ mx));
    1.35 +    parens (n ^ ", " ^ brackets (Library.commas_quote Ts) ^ ", " ^ mx));
    1.36    val opt_name = optional ("(" $$-- name --$$ ")" >> Some) None
    1.37  
    1.38    fun optlistlist s = optional (s $$-- enum "and" (list name)) [[]]
    1.39 @@ -199,7 +199,7 @@
    1.40  (** primrec **)
    1.41  
    1.42  fun mk_patterns eqns = mk_list (map (fn (s, _) => if s = "" then "_" else s) eqns);
    1.43 -fun mk_eqns eqns = mk_list (map (fn (x, y) => mk_pair (mk_pair (quote x, y), "[]")) eqns);
    1.44 +fun mk_eqns eqns = mk_list (map (fn (x, y) => mk_pair (mk_pair (Library.quote x, y), "[]")) eqns);
    1.45  
    1.46  fun mk_primrec_decl (alt_name, eqns) =
    1.47    ";\nval (thy, " ^ mk_patterns eqns ^ ") = PrimrecPackage.add_primrec " ^ alt_name ^ " "
    1.48 @@ -221,7 +221,7 @@
    1.49      ";\n\n\
    1.50      \local\n\
    1.51      \fun simpset() = Simplifier.simpset_of thy;\n\
    1.52 -    \val (thy, result) = thy |> RecdefPackage.add_recdef_old " ^ quote fid ^ " " ^ rel ^ "\n" ^
    1.53 +    \val (thy, result) = thy |> RecdefPackage.add_recdef_old " ^ Library.quote fid ^ " " ^ rel ^ "\n" ^
    1.54      mk_eqns eqns ^ "\n(" ^ ss ^ ",\n " ^ mk_list congs ^ ");\n\
    1.55      \in\n\
    1.56      \structure " ^ fid ^ " =\n\
    1.57 @@ -251,7 +251,7 @@
    1.58    in
    1.59      ";\n\n\
    1.60      \local\n\
    1.61 -    \val (thy, result) = thy |> RecdefPackage.defer_recdef " ^ quote fid ^ "\n" ^
    1.62 +    \val (thy, result) = thy |> RecdefPackage.defer_recdef " ^ Library.quote fid ^ "\n" ^
    1.63      axms_text ^ "\n" ^ congs_text ^ ";\n\
    1.64      \in\n\
    1.65      \structure " ^ fid ^ " =\n\