src/Pure/ProofGeneral/pgip_input.ML
changeset 21940 fbd068dd4d29
parent 21867 8750fbc28d5c
child 22083 4bfd987b005c
     1.1 --- a/src/Pure/ProofGeneral/pgip_input.ML	Fri Dec 29 18:25:45 2006 +0100
     1.2 +++ b/src/Pure/ProofGeneral/pgip_input.ML	Fri Dec 29 18:25:46 2006 +0100
     1.3 @@ -2,7 +2,7 @@
     1.4      ID:         $Id$
     1.5      Author:     David Aspinall
     1.6  
     1.7 -PGIP abstraction: input commands
     1.8 +PGIP abstraction: input commands.
     1.9  *)
    1.10  
    1.11  signature PGIPINPUT =
    1.12 @@ -146,7 +146,7 @@
    1.13      val times_attr = read_pgipnat o (get_attr_dflt "times" "1")
    1.14      val prefcat_attr = get_attr_opt "prefcategory"
    1.15  
    1.16 -    fun xmltext ((XML.Text text)::ts) = text ^ (xmltext ts)
    1.17 +    fun xmltext (XML.Text text :: ts) = text ^ xmltext ts
    1.18        | xmltext [] = ""
    1.19        | xmltext _ = raise PGIP "Expected text (PCDATA/CDATA)"
    1.20