src/HOL/Library/Code_Test.thy
changeset 58637 3094b0edd6b5
parent 58626 6c473ed0ac70
child 58719 ac4f764c5be1
     1.1 --- a/src/HOL/Library/Code_Test.thy	Wed Oct 08 18:10:17 2014 +0200
     1.2 +++ b/src/HOL/Library/Code_Test.thy	Thu Oct 09 11:00:40 2014 +0200
     1.3 @@ -131,10 +131,10 @@
     1.4    "xml_of_term (Code_Evaluation.Const x ty) = [xml.tagged (STR ''0'') (Some x) (xml_of_typ ty)]"
     1.5    "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)]]"
     1.6    "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)]]"
     1.7 -  -- {*
     1.8 -    FIXME: @{const Code_Evaluation.Free} is used only in Quickcheck_Narrowing to represent
     1.9 +  (*
    1.10 +    FIXME: @{const Code_Evaluation.Free} is used only in @{theory Quickcheck_Narrowing} to represent
    1.11      uninstantiated parameters in constructors. Here, we always translate them to @{ML Free} variables.
    1.12 -  *}
    1.13 +  *)
    1.14    "xml_of_term (Code_Evaluation.Free x ty)  = [xml.tagged (STR ''1'') (Some x) (xml_of_typ ty)]"
    1.15  by(simp_all add: xml_of_term_def xml_tree_anything)
    1.16