# HG changeset patch
# User wenzelm
# Date 1237745458 -3600
# Node ID a7d175c48228f094cad2eeed820b9177aa9f6873
# Parent  bc3c1b7df4ec830f5fb7880518a9b7c093b66a14
replaced Antiquote.is_antiq by Antiquote.is_text;

diff -r bc3c1b7df4ec -r a7d175c48228 src/Pure/General/antiquote.ML
--- a/src/Pure/General/antiquote.ML	Sat Mar 21 20:39:38 2009 +0100
+++ b/src/Pure/General/antiquote.ML	Sun Mar 22 19:10:58 2009 +0100
@@ -11,7 +11,7 @@
     Antiq of Symbol_Pos.T list * Position.T |
     Open of Position.T |
     Close of Position.T
-  val is_antiq: 'a antiquote -> bool
+  val is_text: 'a antiquote -> bool
   val scan: Symbol_Pos.T list -> 'a antiquote * Symbol_Pos.T list
   val scan_text: Symbol_Pos.T list -> Symbol_Pos.T list antiquote * Symbol_Pos.T list
   val read: ('a -> unit) -> (Symbol_Pos.T list -> 'a antiquote * Symbol_Pos.T list) ->
@@ -29,8 +29,8 @@
   Open of Position.T |
   Close of Position.T;
 
-fun is_antiq (Text _) = false
-  | is_antiq _ = true;
+fun is_text (Text _) = true
+  | is_text _ = false;
 
 
 (* check_nesting *)
diff -r bc3c1b7df4ec -r a7d175c48228 src/Pure/Thy/thy_output.ML
--- a/src/Pure/Thy/thy_output.ML	Sat Mar 21 20:39:38 2009 +0100
+++ b/src/Pure/Thy/thy_output.ML	Sun Mar 22 19:10:58 2009 +0100
@@ -158,7 +158,7 @@
       | expand (Antiquote.Close _) = "";
     val ants = Antiquote.read (K ()) Antiquote.scan_text (Symbol_Pos.explode (txt, pos), pos);
   in
-    if Toplevel.is_toplevel state andalso exists Antiquote.is_antiq ants then
+    if Toplevel.is_toplevel state andalso not (forall Antiquote.is_text ants) then
       error ("Unknown context -- cannot expand document antiquotations" ^ Position.str_of pos)
     else implode (map expand ants)
   end;