src/ZF/thy_syntax.ML
changeset 6642 732af87c0650
parent 6112 5e4871c5136b
child 8127 68c6159440f1
     1.1 --- a/src/ZF/thy_syntax.ML	Wed May 12 16:54:31 1999 +0200
     1.2 +++ b/src/ZF/thy_syntax.ML	Wed May 12 17:26:56 1999 +0200
     1.3 @@ -23,8 +23,8 @@
     1.4    a list of identifiers.*)
     1.5  fun optlist s = 
     1.6      optional (s $$-- 
     1.7 -	      (string >> strip_quotes
     1.8 -	       || list1 (name>>strip_quotes) >> mk_list)) 
     1.9 +	      (string >> unenclose
    1.10 +	       || list1 (name>>unenclose) >> mk_list)) 
    1.11      "[]";
    1.12  
    1.13  
    1.14 @@ -34,7 +34,7 @@
    1.15      fun mk_params ((((((recs, sdom_sum), ipairs), 
    1.16                        monos), con_defs), type_intrs), type_elims) =
    1.17        let val big_rec_name = space_implode "_" 
    1.18 -                           (map (scan_to_id o strip_quotes) recs)
    1.19 +                           (map (scan_to_id o unenclose) recs)
    1.20            and srec_tms = mk_list recs
    1.21            and sintrs   = mk_big_list (map snd ipairs)
    1.22            and inames   = mk_list (map (mk_intr_name "" o fst) ipairs)
    1.23 @@ -80,11 +80,11 @@
    1.24      val mk_data = mk_list o map mk_const o snd
    1.25      val mk_scons = mk_big_list o map mk_data
    1.26      fun mk_params ((((sdom, rec_pairs), monos), type_intrs), type_elims) =
    1.27 -      let val rec_names = map (scan_to_id o strip_quotes o fst) rec_pairs
    1.28 +      let val rec_names = map (scan_to_id o unenclose o fst) rec_pairs
    1.29  	  val big_rec_name = space_implode "_" rec_names
    1.30  	  and srec_tms = mk_list (map fst rec_pairs)
    1.31  	  and scons    = mk_scons rec_pairs
    1.32 -	  val con_names = flat (map (map (strip_quotes o #1 o #1) o snd)
    1.33 +	  val con_names = flat (map (map (unenclose o #1 o #1) o snd)
    1.34  				rec_pairs)
    1.35            val inames = mk_list (map (mk_intr_name "_I") con_names)
    1.36        in