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

     2.1 --- a/src/HOLCF/domain/interface.ML	Wed May 12 16:54:31 1999 +0200
     2.2 +++ b/src/HOLCF/domain/interface.ML	Wed May 12 17:26:56 1999 +0200
     2.3 @@ -102,8 +102,8 @@
     2.4  
     2.5  (* ----- parser for domain declaration equation ----------------------------- *)
     2.6  
     2.7 -  val name' = name >> strip_quotes;
     2.8 -  val type_var' = type_var >> strip_quotes;
     2.9 +  val name' = name >> unenclose;
    2.10 +  val type_var' = type_var >> unenclose;
    2.11    fun esc_quote s = let fun esc [] = []
    2.12  			|   esc ("\""::xs) = esc xs
    2.13  			|   esc ("[" ::xs) = "{"::esc xs

     3.1 --- a/src/Pure/Thy/thy_parse.ML	Wed May 12 16:54:31 1999 +0200
     3.2 +++ b/src/Pure/Thy/thy_parse.ML	Wed May 12 17:26:56 1999 +0200
     3.3 @@ -70,7 +70,6 @@
     3.4    val mk_triple: string * string * string -> string
     3.5    val mk_triple1: (string * string) * string -> string
     3.6    val mk_triple2: string * (string * string) -> string
     3.7 -  val strip_quotes: string -> string
     3.8  end;
     3.9  
    3.10  
    3.11 @@ -178,10 +177,6 @@
    3.12  
    3.13  fun split_decls l = flat (map (fn (xs, y) => map (rpair y) xs) l);
    3.14  
    3.15 -(*Remove the leading and trailing chararacters.  Actually called to
    3.16 -  remove quotation marks.*)
    3.17 -fun strip_quotes s = String.substring (s, 1, size s - 2);
    3.18 -
    3.19  
    3.20  (* names *)
    3.21  
    3.22 @@ -393,8 +388,7 @@
    3.23  (* axclass *)
    3.24  
    3.25  fun mk_axclass_decl ((c, cs), axms) =
    3.26 -  (mk_pair (c, cs) ^ "\n" ^ mk_axms' axms,
    3.27 -    strip_quotes c ^ "I" :: map fst axms);
    3.28 +  (mk_pair (c, cs) ^ "\n" ^ mk_axms' axms, unenclose c ^ "I" :: map fst axms);
    3.29  
    3.30  val axclass_decl = subclass -- repeat (ident -- !! string) >> mk_axclass_decl;
    3.31  

     4.1 --- a/src/Pure/library.ML	Wed May 12 16:54:31 1999 +0200
     4.2 +++ b/src/Pure/library.ML	Wed May 12 17:26:56 1999 +0200
     4.3 @@ -127,6 +127,7 @@
     4.4    val foldl_string: ('a * string -> 'a) -> 'a * string -> 'a
     4.5    val exists_string: (string -> bool) -> string -> bool
     4.6    val enclose: string -> string -> string -> string
     4.7 +  val unenclose: string -> string
     4.8    val quote: string -> string
     4.9    val space_implode: string -> string list -> string
    4.10    val commas: string list -> string
    4.11 @@ -673,6 +674,7 @@
    4.12  
    4.13  (*enclose in brackets*)
    4.14  fun enclose lpar rpar str = lpar ^ str ^ rpar;
    4.15 +fun unenclose str = String.substring (str, 1, size str - 2);
    4.16  
    4.17  (*simple quoting (does not escape special chars)*)
    4.18  val quote = enclose "\"" "\"";

     5.1 --- a/src/ZF/thy_syntax.ML	Wed May 12 16:54:31 1999 +0200
     5.2 +++ b/src/ZF/thy_syntax.ML	Wed May 12 17:26:56 1999 +0200
     5.3 @@ -23,8 +23,8 @@
     5.4    a list of identifiers.*)
     5.5  fun optlist s = 
     5.6      optional (s $$-- 
     5.7 -	      (string >> strip_quotes
     5.8 -	       || list1 (name>>strip_quotes) >> mk_list)) 
     5.9 +	      (string >> unenclose
    5.10 +	       || list1 (name>>unenclose) >> mk_list)) 
    5.11      "[]";
    5.12  
    5.13  
    5.14 @@ -34,7 +34,7 @@
    5.15      fun mk_params ((((((recs, sdom_sum), ipairs), 
    5.16                        monos), con_defs), type_intrs), type_elims) =
    5.17        let val big_rec_name = space_implode "_" 
    5.18 -                           (map (scan_to_id o strip_quotes) recs)
    5.19 +                           (map (scan_to_id o unenclose) recs)
    5.20            and srec_tms = mk_list recs
    5.21            and sintrs   = mk_big_list (map snd ipairs)
    5.22            and inames   = mk_list (map (mk_intr_name "" o fst) ipairs)
    5.23 @@ -80,11 +80,11 @@
    5.24      val mk_data = mk_list o map mk_const o snd
    5.25      val mk_scons = mk_big_list o map mk_data
    5.26      fun mk_params ((((sdom, rec_pairs), monos), type_intrs), type_elims) =
    5.27 -      let val rec_names = map (scan_to_id o strip_quotes o fst) rec_pairs
    5.28 +      let val rec_names = map (scan_to_id o unenclose o fst) rec_pairs
    5.29  	  val big_rec_name = space_implode "_" rec_names
    5.30  	  and srec_tms = mk_list (map fst rec_pairs)
    5.31  	  and scons    = mk_scons rec_pairs
    5.32 -	  val con_names = flat (map (map (strip_quotes o #1 o #1) o snd)
    5.33 +	  val con_names = flat (map (map (unenclose o #1 o #1) o snd)
    5.34  				rec_pairs)
    5.35            val inames = mk_list (map (mk_intr_name "_I") con_names)
    5.36        in