# HG changeset patch
# User wenzelm
# Date 1120672856 -7200
# Node ID 124b4782944fa6ea9f515c84b7f9972b7e7afe69
# Parent  ff304c52bf86213766270fec56565d662aa8f933
fixed antiquotation;

diff -r ff304c52bf86 -r 124b4782944f src/HOL/ex/Primrec.thy
--- a/src/HOL/ex/Primrec.thy	Wed Jul 06 20:00:42 2005 +0200
+++ b/src/HOL/ex/Primrec.thy	Wed Jul 06 20:00:56 2005 +0200
@@ -287,7 +287,7 @@
   apply (unfold COMP_def)
   apply (frule Int_lower1 [THEN lists_mono, THEN subsetD])
     --{*Now, if meson tolerated map, we could finish with
-  @{text "(drule COMP_map_aux, meson ack_less_mono2 ack_nest_bound less_trans).*}
+  @{text "(drule COMP_map_aux, meson ack_less_mono2 ack_nest_bound less_trans)"} *}
   apply (erule COMP_map_aux [THEN exE])
   apply (rule exI)
   apply (rule allI)