# HG changeset patch
# User wenzelm
# Date 926522816 -7200
# Node ID 732af87c0650cdda6b982754056fb036a25b4e14
# Parent  254ab03bd08289e414e62bdd1dda0926feba0742
strip_quotes replaced by unenclose;

diff -r 254ab03bd082 -r 732af87c0650 src/HOL/thy_syntax.ML
--- a/src/HOL/thy_syntax.ML	Wed May 12 16:54:31 1999 +0200
+++ b/src/HOL/thy_syntax.ML	Wed May 12 17:26:56 1999 +0200
@@ -15,7 +15,7 @@
 fun mk_typedef_decl (((((opt_name, vs), t), mx), rhs), wt) =
   let
     val name' = if_none opt_name t;
-    val name = strip_quotes name';
+    val name = unenclose name';
   in
     (cat_lines [name', mk_triple (t, mk_list vs, mx), rhs, wt],
       [name ^ "_def", "Rep_" ^ name, "Rep_" ^ name ^ "_inverse",
@@ -47,7 +47,7 @@
     fun mk_intr_name (s, _) =   (*the "op" cancels any infix status*)
       if Syntax.is_identifier s then "op " ^ s else "_";
     fun mk_params (((recs, ipairs), monos), con_defs) =
-      let val big_rec_name = space_implode "_" (map (scan_to_id o strip_quotes) recs)
+      let val big_rec_name = space_implode "_" (map (scan_to_id o unenclose) recs)
           and srec_tms = mk_list recs
           and sintrs   = mk_big_list (no_atts (map (mk_pair o apfst quote) ipairs))
       in
@@ -126,7 +126,7 @@
   fun mk_dt_string dts =
     let
       val names = map (fn ((((alt_name, _), name), _), _) =>
-        strip_quotes (if_none alt_name name)) dts;
+        unenclose (if_none alt_name name)) dts;
 
       val add_datatype_args = brackets (commas (map quote names)) ^ " " ^
         brackets (commas (map (fn ((((_, vs), name), mx), cs) =>
@@ -160,7 +160,7 @@
 
   (*** parsers ***)
 
-  val simple_typ = ident || (type_var >> strip_quotes);
+  val simple_typ = ident || (type_var >> unenclose);
 
   fun complex_typ toks =
     let val typ = simple_typ || "(" $$-- complex_typ --$$ ")";
@@ -171,7 +171,7 @@
         (repeat1 ident >> (cat "" o space_implode " "))) toks
     end;
 
-  val opt_typs = repeat ((string >> strip_quotes) ||
+  val opt_typs = repeat ((string >> unenclose) ||
     simple_typ || ("(" $$-- complex_typ --$$ ")"));
   val constructor = name -- opt_typs -- opt_mixfix >> (fn ((n, Ts), mx) =>
     parens (n ^ ", " ^ brackets (commas_quote Ts) ^ ", " ^ mx));
@@ -184,7 +184,7 @@
     enum1 "and" (opt_name -- type_args -- name -- opt_infix --$$ "=" --
       enum1 "|" constructor) >> mk_dt_string;
   val rep_datatype_decl =
-    ((optional ((repeat1 (name >> strip_quotes)) >> Some) None) --
+    ((optional ((repeat1 (name >> unenclose)) >> Some) None) --
       optlistlist "distinct" -- optlistlist "inject" --
         ("induct" $$-- name)) >> mk_rep_dt_string;
 end;
@@ -215,7 +215,7 @@
 (*fname: name of function being defined; rel: well-founded relation*)
 fun mk_recdef_decl ((((fname, rel), congs), ss), axms) =
   let
-    val fid = strip_quotes fname;
+    val fid = unenclose fname;
     val congs_text = mk_list (map (fn c => mk_pair (c, "[]")) congs);
     val axms_text = mk_big_list axms;
   in
@@ -236,7 +236,7 @@
 val recdef_decl =
   (name -- string --
     optional ("congs" $$-- list1 name) [] --
-    optional ("simpset" $$-- string >> strip_quotes) "simpset()" --
+    optional ("simpset" $$-- string >> unenclose) "simpset()" --
     repeat1 string >> mk_recdef_decl);
 
 
@@ -245,7 +245,7 @@
 (*fname: name of function being defined; rel: well-founded relation*)
 fun mk_defer_recdef_decl ((fname, congs), axms) =
   let
-    val fid = strip_quotes fname;
+    val fid = unenclose fname;
     val congs_text = mk_list (map (fn c => mk_pair (c, "[]")) congs);
     val axms_text = mk_big_list axms;
   in
diff -r 254ab03bd082 -r 732af87c0650 src/HOLCF/domain/interface.ML
--- a/src/HOLCF/domain/interface.ML	Wed May 12 16:54:31 1999 +0200
+++ b/src/HOLCF/domain/interface.ML	Wed May 12 17:26:56 1999 +0200
@@ -102,8 +102,8 @@
 
 (* ----- parser for domain declaration equation ----------------------------- *)
 
-  val name' = name >> strip_quotes;
-  val type_var' = type_var >> strip_quotes;
+  val name' = name >> unenclose;
+  val type_var' = type_var >> unenclose;
   fun esc_quote s = let fun esc [] = []
 			|   esc ("\""::xs) = esc xs
 			|   esc ("[" ::xs) = "{"::esc xs
diff -r 254ab03bd082 -r 732af87c0650 src/Pure/Thy/thy_parse.ML
--- a/src/Pure/Thy/thy_parse.ML	Wed May 12 16:54:31 1999 +0200
+++ b/src/Pure/Thy/thy_parse.ML	Wed May 12 17:26:56 1999 +0200
@@ -70,7 +70,6 @@
   val mk_triple: string * string * string -> string
   val mk_triple1: (string * string) * string -> string
   val mk_triple2: string * (string * string) -> string
-  val strip_quotes: string -> string
 end;
 
 
@@ -178,10 +177,6 @@
 
 fun split_decls l = flat (map (fn (xs, y) => map (rpair y) xs) l);
 
-(*Remove the leading and trailing chararacters.  Actually called to
-  remove quotation marks.*)
-fun strip_quotes s = String.substring (s, 1, size s - 2);
-
 
 (* names *)
 
@@ -393,8 +388,7 @@
 (* axclass *)
 
 fun mk_axclass_decl ((c, cs), axms) =
-  (mk_pair (c, cs) ^ "\n" ^ mk_axms' axms,
-    strip_quotes c ^ "I" :: map fst axms);
+  (mk_pair (c, cs) ^ "\n" ^ mk_axms' axms, unenclose c ^ "I" :: map fst axms);
 
 val axclass_decl = subclass -- repeat (ident -- !! string) >> mk_axclass_decl;
 
diff -r 254ab03bd082 -r 732af87c0650 src/Pure/library.ML
--- a/src/Pure/library.ML	Wed May 12 16:54:31 1999 +0200
+++ b/src/Pure/library.ML	Wed May 12 17:26:56 1999 +0200
@@ -127,6 +127,7 @@
   val foldl_string: ('a * string -> 'a) -> 'a * string -> 'a
   val exists_string: (string -> bool) -> string -> bool
   val enclose: string -> string -> string -> string
+  val unenclose: string -> string
   val quote: string -> string
   val space_implode: string -> string list -> string
   val commas: string list -> string
@@ -673,6 +674,7 @@
 
 (*enclose in brackets*)
 fun enclose lpar rpar str = lpar ^ str ^ rpar;
+fun unenclose str = String.substring (str, 1, size str - 2);
 
 (*simple quoting (does not escape special chars)*)
 val quote = enclose "\"" "\"";
diff -r 254ab03bd082 -r 732af87c0650 src/ZF/thy_syntax.ML
--- a/src/ZF/thy_syntax.ML	Wed May 12 16:54:31 1999 +0200
+++ b/src/ZF/thy_syntax.ML	Wed May 12 17:26:56 1999 +0200
@@ -23,8 +23,8 @@
   a list of identifiers.*)
 fun optlist s = 
     optional (s $$-- 
-	      (string >> strip_quotes
-	       || list1 (name>>strip_quotes) >> mk_list)) 
+	      (string >> unenclose
+	       || list1 (name>>unenclose) >> mk_list)) 
     "[]";
 
 
@@ -34,7 +34,7 @@
     fun mk_params ((((((recs, sdom_sum), ipairs), 
                       monos), con_defs), type_intrs), type_elims) =
       let val big_rec_name = space_implode "_" 
-                           (map (scan_to_id o strip_quotes) recs)
+                           (map (scan_to_id o unenclose) recs)
           and srec_tms = mk_list recs
           and sintrs   = mk_big_list (map snd ipairs)
           and inames   = mk_list (map (mk_intr_name "" o fst) ipairs)
@@ -80,11 +80,11 @@
     val mk_data = mk_list o map mk_const o snd
     val mk_scons = mk_big_list o map mk_data
     fun mk_params ((((sdom, rec_pairs), monos), type_intrs), type_elims) =
-      let val rec_names = map (scan_to_id o strip_quotes o fst) rec_pairs
+      let val rec_names = map (scan_to_id o unenclose o fst) rec_pairs
 	  val big_rec_name = space_implode "_" rec_names
 	  and srec_tms = mk_list (map fst rec_pairs)
 	  and scons    = mk_scons rec_pairs
-	  val con_names = flat (map (map (strip_quotes o #1 o #1) o snd)
+	  val con_names = flat (map (map (unenclose o #1 o #1) o snd)
 				rec_pairs)
           val inames = mk_list (map (mk_intr_name "_I") con_names)
       in