src/Pure/proof_general.ML
changeset 19473 d87a8838afa4
parent 19300 7689f81f8996
child 19482 9f11af8f7ef9
     1.1 --- a/src/Pure/proof_general.ML	Wed Apr 26 20:34:11 2006 +0200
     1.2 +++ b/src/Pure/proof_general.ML	Wed Apr 26 22:38:05 2006 +0200
     1.3 @@ -172,12 +172,12 @@
     1.4          ("class",  pgip_class),
     1.5          ("seq",    string_of_int (pgip_serial())),
     1.6          ("id",     !pgip_id)] @
     1.7 -       if_none (Option.map (single o (pair "destid")) (! pgip_refid)) [] @
     1.8 +       the_default [] (Option.map (single o (pair "destid")) (! pgip_refid)) @
     1.9         (* destid=refid since Isabelle only communicates back to sender,
    1.10            so we may omit refid from attributes.
    1.11 -       if_none (Option.map (single o (pair "refid"))  (! pgip_refid)) [] @
    1.12 +       the_default [] (Option.map (single o (pair "refid"))  (! pgip_refid)) @
    1.13         *)
    1.14 -       if_none (Option.map (single o (pair "refseq")) (! pgip_refseq)) [])
    1.15 +       the_default [] (Option.map (single o (pair "refseq")) (! pgip_refseq)))
    1.16        pgips;
    1.17  
    1.18  in
    1.19 @@ -1102,7 +1102,7 @@
    1.20                                                ("default", default)]
    1.21                         [ty]) prefs)]) (!preferences)
    1.22  
    1.23 -fun allprefs () = Library.foldl (op @) ([], map snd (!preferences))
    1.24 +fun allprefs () = maps snd (!preferences)
    1.25  
    1.26  fun setpref name value =
    1.27      (case AList.lookup (op =) (allprefs ()) name of