replaced obsolete "trim" by "strip_quotes"
authorpaulson
Mon Dec 28 16:46:15 1998 +0100 (1998-12-28)
changeset 6035c041fc54ab4c
parent 6034 96ac04a17c56
child 6036 1512f4b7d2e8
replaced obsolete "trim" by "strip_quotes"
src/HOL/thy_syntax.ML
     1.1 --- a/src/HOL/thy_syntax.ML	Fri Dec 18 19:43:10 1998 +0100
     1.2 +++ b/src/HOL/thy_syntax.ML	Mon Dec 28 16:46:15 1998 +0100
     1.3 @@ -45,7 +45,7 @@
     1.4      fun mk_intr_name (s, _) =   (*the "op" cancels any infix status*)
     1.5        if Syntax.is_identifier s then "op " ^ s else "_";
     1.6      fun mk_params (((recs, ipairs), monos), con_defs) =
     1.7 -      let val big_rec_name = space_implode "_" (map (scan_to_id o trim) recs)
     1.8 +      let val big_rec_name = space_implode "_" (map (scan_to_id o strip_quotes) recs)
     1.9            and srec_tms = mk_list recs
    1.10            and sintrs   = mk_big_list (map snd ipairs)
    1.11        in
    1.12 @@ -206,7 +206,7 @@
    1.13  
    1.14  (*fname: name of function being defined; rel: well-founded relation*)
    1.15  fun mk_rec_decl ((((fname, rel), congs), ss), axms) =
    1.16 -  let val fid = trim fname
    1.17 +  let val fid = strip_quotes fname
    1.18        val intrnl_name = fid ^ "_Intrnl"
    1.19    in
    1.20  	 (";\n\n\
    1.21 @@ -226,10 +226,11 @@
    1.22            \val pats_" ^ intrnl_name ^ " = ();\n")
    1.23    end;
    1.24  
    1.25 -val rec_decl = (name -- string -- 
    1.26 -		optional ("congs" $$-- string >> trim) "[]" -- 
    1.27 -		optional ("simpset" $$-- string >> trim) "simpset()" -- 
    1.28 -		repeat1 string >> mk_rec_decl) ;
    1.29 +val rec_decl = 
    1.30 +    (name -- string -- 
    1.31 +     optional ("congs" $$-- string >> strip_quotes) "[]" -- 
    1.32 +     optional ("simpset" $$-- string >> strip_quotes) "simpset()" -- 
    1.33 +     repeat1 string >> mk_rec_decl) ;
    1.34  
    1.35  
    1.36