# HG changeset patch
# User paulson
# Date 914859975 -3600
# Node ID c041fc54ab4c6e04add4d0c3821406c0318511fc
# Parent  96ac04a17c5621c2fdd065a66e4c2fe85e22ee30
replaced obsolete "trim" by "strip_quotes"

diff -r 96ac04a17c56 -r c041fc54ab4c src/HOL/thy_syntax.ML
--- a/src/HOL/thy_syntax.ML	Fri Dec 18 19:43:10 1998 +0100
+++ b/src/HOL/thy_syntax.ML	Mon Dec 28 16:46:15 1998 +0100
@@ -45,7 +45,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 trim) recs)
+      let val big_rec_name = space_implode "_" (map (scan_to_id o strip_quotes) recs)
           and srec_tms = mk_list recs
           and sintrs   = mk_big_list (map snd ipairs)
       in
@@ -206,7 +206,7 @@
 
 (*fname: name of function being defined; rel: well-founded relation*)
 fun mk_rec_decl ((((fname, rel), congs), ss), axms) =
-  let val fid = trim fname
+  let val fid = strip_quotes fname
       val intrnl_name = fid ^ "_Intrnl"
   in
 	 (";\n\n\
@@ -226,10 +226,11 @@
           \val pats_" ^ intrnl_name ^ " = ();\n")
   end;
 
-val rec_decl = (name -- string -- 
-		optional ("congs" $$-- string >> trim) "[]" -- 
-		optional ("simpset" $$-- string >> trim) "simpset()" -- 
-		repeat1 string >> mk_rec_decl) ;
+val rec_decl = 
+    (name -- string -- 
+     optional ("congs" $$-- string >> strip_quotes) "[]" -- 
+     optional ("simpset" $$-- string >> strip_quotes) "simpset()" -- 
+     repeat1 string >> mk_rec_decl) ;