src/HOL/thy_syntax.ML
changeset 6642 732af87c0650
parent 6576 7e0b35bed503
child 8623 5668aaf41c36
     1.1 --- a/src/HOL/thy_syntax.ML	Wed May 12 16:54:31 1999 +0200
     1.2 +++ b/src/HOL/thy_syntax.ML	Wed May 12 17:26:56 1999 +0200
     1.3 @@ -15,7 +15,7 @@
     1.4  fun mk_typedef_decl (((((opt_name, vs), t), mx), rhs), wt) =
     1.5    let
     1.6      val name' = if_none opt_name t;
     1.7 -    val name = strip_quotes name';
     1.8 +    val name = unenclose name';
     1.9    in
    1.10      (cat_lines [name', mk_triple (t, mk_list vs, mx), rhs, wt],
    1.11        [name ^ "_def", "Rep_" ^ name, "Rep_" ^ name ^ "_inverse",
    1.12 @@ -47,7 +47,7 @@
    1.13      fun mk_intr_name (s, _) =   (*the "op" cancels any infix status*)
    1.14        if Syntax.is_identifier s then "op " ^ s else "_";
    1.15      fun mk_params (((recs, ipairs), monos), con_defs) =
    1.16 -      let val big_rec_name = space_implode "_" (map (scan_to_id o strip_quotes) recs)
    1.17 +      let val big_rec_name = space_implode "_" (map (scan_to_id o unenclose) recs)
    1.18            and srec_tms = mk_list recs
    1.19            and sintrs   = mk_big_list (no_atts (map (mk_pair o apfst quote) ipairs))
    1.20        in
    1.21 @@ -126,7 +126,7 @@
    1.22    fun mk_dt_string dts =
    1.23      let
    1.24        val names = map (fn ((((alt_name, _), name), _), _) =>
    1.25 -        strip_quotes (if_none alt_name name)) dts;
    1.26 +        unenclose (if_none alt_name name)) dts;
    1.27  
    1.28        val add_datatype_args = brackets (commas (map quote names)) ^ " " ^
    1.29          brackets (commas (map (fn ((((_, vs), name), mx), cs) =>
    1.30 @@ -160,7 +160,7 @@
    1.31  
    1.32    (*** parsers ***)
    1.33  
    1.34 -  val simple_typ = ident || (type_var >> strip_quotes);
    1.35 +  val simple_typ = ident || (type_var >> unenclose);
    1.36  
    1.37    fun complex_typ toks =
    1.38      let val typ = simple_typ || "(" $$-- complex_typ --$$ ")";
    1.39 @@ -171,7 +171,7 @@
    1.40          (repeat1 ident >> (cat "" o space_implode " "))) toks
    1.41      end;
    1.42  
    1.43 -  val opt_typs = repeat ((string >> strip_quotes) ||
    1.44 +  val opt_typs = repeat ((string >> unenclose) ||
    1.45      simple_typ || ("(" $$-- complex_typ --$$ ")"));
    1.46    val constructor = name -- opt_typs -- opt_mixfix >> (fn ((n, Ts), mx) =>
    1.47      parens (n ^ ", " ^ brackets (commas_quote Ts) ^ ", " ^ mx));
    1.48 @@ -184,7 +184,7 @@
    1.49      enum1 "and" (opt_name -- type_args -- name -- opt_infix --$$ "=" --
    1.50        enum1 "|" constructor) >> mk_dt_string;
    1.51    val rep_datatype_decl =
    1.52 -    ((optional ((repeat1 (name >> strip_quotes)) >> Some) None) --
    1.53 +    ((optional ((repeat1 (name >> unenclose)) >> Some) None) --
    1.54        optlistlist "distinct" -- optlistlist "inject" --
    1.55          ("induct" $$-- name)) >> mk_rep_dt_string;
    1.56  end;
    1.57 @@ -215,7 +215,7 @@
    1.58  (*fname: name of function being defined; rel: well-founded relation*)
    1.59  fun mk_recdef_decl ((((fname, rel), congs), ss), axms) =
    1.60    let
    1.61 -    val fid = strip_quotes fname;
    1.62 +    val fid = unenclose fname;
    1.63      val congs_text = mk_list (map (fn c => mk_pair (c, "[]")) congs);
    1.64      val axms_text = mk_big_list axms;
    1.65    in
    1.66 @@ -236,7 +236,7 @@
    1.67  val recdef_decl =
    1.68    (name -- string --
    1.69      optional ("congs" $$-- list1 name) [] --
    1.70 -    optional ("simpset" $$-- string >> strip_quotes) "simpset()" --
    1.71 +    optional ("simpset" $$-- string >> unenclose) "simpset()" --
    1.72      repeat1 string >> mk_recdef_decl);
    1.73  
    1.74  
    1.75 @@ -245,7 +245,7 @@
    1.76  (*fname: name of function being defined; rel: well-founded relation*)
    1.77  fun mk_defer_recdef_decl ((fname, congs), axms) =
    1.78    let
    1.79 -    val fid = strip_quotes fname;
    1.80 +    val fid = unenclose fname;
    1.81      val congs_text = mk_list (map (fn c => mk_pair (c, "[]")) congs);
    1.82      val axms_text = mk_big_list axms;
    1.83    in