# HG changeset patch
# User wenzelm
# Date 1412868710 -7200
# Node ID 8d108c0e7da240ba7634948f9cfbb846a5ed0c3d
# Parent  3094b0edd6b52a6c9b85e91147bdb6e475dc1531# Parent  5697ae9a683a10a7cf854d8a60a04df93cb0104d
merged

diff -r 5697ae9a683a -r 8d108c0e7da2 src/HOL/Library/Code_Test.thy
--- a/src/HOL/Library/Code_Test.thy	Thu Oct 09 13:57:40 2014 +0200
+++ b/src/HOL/Library/Code_Test.thy	Thu Oct 09 17:31:50 2014 +0200
@@ -131,10 +131,10 @@
   "xml_of_term (Code_Evaluation.Const x ty) = [xml.tagged (STR ''0'') (Some x) (xml_of_typ ty)]"
   "xml_of_term (Code_Evaluation.App t1 t2)  = [xml.tagged (STR ''5'') None [xml.node (xml_of_term t1), xml.node (xml_of_term t2)]]"
   "xml_of_term (Code_Evaluation.Abs x ty t) = [xml.tagged (STR ''4'') (Some x) [xml.node (xml_of_typ ty), xml.node (xml_of_term t)]]"
-  -- {*
-    FIXME: @{const Code_Evaluation.Free} is used only in Quickcheck_Narrowing to represent
+  (*
+    FIXME: @{const Code_Evaluation.Free} is used only in @{theory Quickcheck_Narrowing} to represent
     uninstantiated parameters in constructors. Here, we always translate them to @{ML Free} variables.
-  *}
+  *)
   "xml_of_term (Code_Evaluation.Free x ty)  = [xml.tagged (STR ''1'') (Some x) (xml_of_typ ty)]"
 by(simp_all add: xml_of_term_def xml_tree_anything)