# HG changeset patch
# User wenzelm
# Date 1211115867 -7200
# Node ID 1fe801f9cfc9a47c3881890c498f2313dae08434
# Parent  aec0d97a01c4f075a8a87785c12fc9c5fc56fc36
Syntax.string_of_term with proper context;

diff -r aec0d97a01c4 -r 1fe801f9cfc9 src/HOL/ex/Quickcheck.thy
--- a/src/HOL/ex/Quickcheck.thy	Sun May 18 15:04:24 2008 +0200
+++ b/src/HOL/ex/Quickcheck.thy	Sun May 18 15:04:27 2008 +0200
@@ -291,91 +291,91 @@
 ML {* val f = Quickcheck.compile_generator_expr @{theory}
   @{term "\<lambda>(n::nat) (m::nat) (q::nat). n = m + q + 1"} [@{typ nat}, @{typ nat}, @{typ nat}] *}
 
-ML {* f 5 |> (Option.map o map) (Sign.string_of_term @{theory}) *}
-ML {* f 5 |> (Option.map o map) (Sign.string_of_term @{theory}) *}
-ML {* f 20 |> (Option.map o map) (Sign.string_of_term @{theory}) *}
-ML {* f 20 |> (Option.map o map) (Sign.string_of_term @{theory}) *}
-ML {* f 20 |> (Option.map o map) (Sign.string_of_term @{theory}) *}
-ML {* f 20 |> (Option.map o map) (Sign.string_of_term @{theory}) *}
-ML {* f 25 |> (Option.map o map) (Sign.string_of_term @{theory}) *}
-ML {* f 1 |> (Option.map o map) (Sign.string_of_term @{theory}) *}
-ML {* f 1 |> (Option.map o map) (Sign.string_of_term @{theory}) *}
-ML {* f 2 |> (Option.map o map) (Sign.string_of_term @{theory}) *}
-ML {* f 2 |> (Option.map o map) (Sign.string_of_term @{theory}) *}
+ML {* f 5 |> (Option.map o map) (Syntax.string_of_term @{context}) *}
+ML {* f 5 |> (Option.map o map) (Syntax.string_of_term @{context}) *}
+ML {* f 20 |> (Option.map o map) (Syntax.string_of_term @{context}) *}
+ML {* f 20 |> (Option.map o map) (Syntax.string_of_term @{context}) *}
+ML {* f 20 |> (Option.map o map) (Syntax.string_of_term @{context}) *}
+ML {* f 20 |> (Option.map o map) (Syntax.string_of_term @{context}) *}
+ML {* f 25 |> (Option.map o map) (Syntax.string_of_term @{context}) *}
+ML {* f 1 |> (Option.map o map) (Syntax.string_of_term @{context}) *}
+ML {* f 1 |> (Option.map o map) (Syntax.string_of_term @{context}) *}
+ML {* f 2 |> (Option.map o map) (Syntax.string_of_term @{context}) *}
+ML {* f 2 |> (Option.map o map) (Syntax.string_of_term @{context}) *}
 
 ML {* val f = Quickcheck.compile_generator_expr @{theory}
   @{term "\<lambda>(n::int) (m::int) (q::int). n = m + q + 1"} [@{typ int}, @{typ int}, @{typ int}] *}
 
-ML {* f 5 |> (Option.map o map) (Sign.string_of_term @{theory}) *}
-ML {* f 5 |> (Option.map o map) (Sign.string_of_term @{theory}) *}
-ML {* f 20 |> (Option.map o map) (Sign.string_of_term @{theory}) *}
-ML {* f 20 |> (Option.map o map) (Sign.string_of_term @{theory}) *}
-ML {* f 20 |> (Option.map o map) (Sign.string_of_term @{theory}) *}
-ML {* f 20 |> (Option.map o map) (Sign.string_of_term @{theory}) *}
-ML {* f 25 |> (Option.map o map) (Sign.string_of_term @{theory}) *}
-ML {* f 1 |> (Option.map o map) (Sign.string_of_term @{theory}) *}
-ML {* f 1 |> (Option.map o map) (Sign.string_of_term @{theory}) *}
-ML {* f 2 |> (Option.map o map) (Sign.string_of_term @{theory}) *}
-ML {* f 2 |> (Option.map o map) (Sign.string_of_term @{theory}) *}
-ML {* f 3 |> (Option.map o map) (Sign.string_of_term @{theory}) *}
-ML {* f 4 |> (Option.map o map) (Sign.string_of_term @{theory}) *}
-ML {* f 4 |> (Option.map o map) (Sign.string_of_term @{theory}) *}
+ML {* f 5 |> (Option.map o map) (Syntax.string_of_term @{context}) *}
+ML {* f 5 |> (Option.map o map) (Syntax.string_of_term @{context}) *}
+ML {* f 20 |> (Option.map o map) (Syntax.string_of_term @{context}) *}
+ML {* f 20 |> (Option.map o map) (Syntax.string_of_term @{context}) *}
+ML {* f 20 |> (Option.map o map) (Syntax.string_of_term @{context}) *}
+ML {* f 20 |> (Option.map o map) (Syntax.string_of_term @{context}) *}
+ML {* f 25 |> (Option.map o map) (Syntax.string_of_term @{context}) *}
+ML {* f 1 |> (Option.map o map) (Syntax.string_of_term @{context}) *}
+ML {* f 1 |> (Option.map o map) (Syntax.string_of_term @{context}) *}
+ML {* f 2 |> (Option.map o map) (Syntax.string_of_term @{context}) *}
+ML {* f 2 |> (Option.map o map) (Syntax.string_of_term @{context}) *}
+ML {* f 3 |> (Option.map o map) (Syntax.string_of_term @{context}) *}
+ML {* f 4 |> (Option.map o map) (Syntax.string_of_term @{context}) *}
+ML {* f 4 |> (Option.map o map) (Syntax.string_of_term @{context}) *}
 
 ML {* val f = Quickcheck.compile_generator_expr @{theory}
   @{term "\<lambda>(xs\<Colon>int list) ys. rev (xs @ ys) = rev xs @ rev ys"}
   [@{typ "int list"}, @{typ "int list"}] *}
 
-ML {* f 15 |> (Option.map o map) (Sign.string_of_term @{theory}) *}
-ML {* f 5 |> (Option.map o map) (Sign.string_of_term @{theory}) *}
-ML {* f 20 |> (Option.map o map) (Sign.string_of_term @{theory}) *}
-ML {* f 20 |> (Option.map o map) (Sign.string_of_term @{theory}) *}
-ML {* f 20 |> (Option.map o map) (Sign.string_of_term @{theory}) *}
-ML {* f 20 |> (Option.map o map) (Sign.string_of_term @{theory}) *}
-ML {* f 25 |> (Option.map o map) (Sign.string_of_term @{theory}) *}
-ML {* f 1 |> (Option.map o map) (Sign.string_of_term @{theory}) *}
-ML {* f 1 |> (Option.map o map) (Sign.string_of_term @{theory}) *}
-ML {* f 2 |> (Option.map o map) (Sign.string_of_term @{theory}) *}
-ML {* f 2 |> (Option.map o map) (Sign.string_of_term @{theory}) *}
-ML {* f 4 |> (Option.map o map) (Sign.string_of_term @{theory}) *}
-ML {* f 4 |> (Option.map o map) (Sign.string_of_term @{theory}) *}
-ML {* f 5 |> (Option.map o map) (Sign.string_of_term @{theory}) *}
-ML {* f 8 |> (Option.map o map) (Sign.string_of_term @{theory}) *}
-ML {* f 8 |> (Option.map o map) (Sign.string_of_term @{theory}) *}
-ML {* f 8 |> (Option.map o map) (Sign.string_of_term @{theory}) *}
-ML {* f 88 |> (Option.map o map) (Sign.string_of_term @{theory}) *}
+ML {* f 15 |> (Option.map o map) (Syntax.string_of_term @{context}) *}
+ML {* f 5 |> (Option.map o map) (Syntax.string_of_term @{context}) *}
+ML {* f 20 |> (Option.map o map) (Syntax.string_of_term @{context}) *}
+ML {* f 20 |> (Option.map o map) (Syntax.string_of_term @{context}) *}
+ML {* f 20 |> (Option.map o map) (Syntax.string_of_term @{context}) *}
+ML {* f 20 |> (Option.map o map) (Syntax.string_of_term @{context}) *}
+ML {* f 25 |> (Option.map o map) (Syntax.string_of_term @{context}) *}
+ML {* f 1 |> (Option.map o map) (Syntax.string_of_term @{context}) *}
+ML {* f 1 |> (Option.map o map) (Syntax.string_of_term @{context}) *}
+ML {* f 2 |> (Option.map o map) (Syntax.string_of_term @{context}) *}
+ML {* f 2 |> (Option.map o map) (Syntax.string_of_term @{context}) *}
+ML {* f 4 |> (Option.map o map) (Syntax.string_of_term @{context}) *}
+ML {* f 4 |> (Option.map o map) (Syntax.string_of_term @{context}) *}
+ML {* f 5 |> (Option.map o map) (Syntax.string_of_term @{context}) *}
+ML {* f 8 |> (Option.map o map) (Syntax.string_of_term @{context}) *}
+ML {* f 8 |> (Option.map o map) (Syntax.string_of_term @{context}) *}
+ML {* f 8 |> (Option.map o map) (Syntax.string_of_term @{context}) *}
+ML {* f 88 |> (Option.map o map) (Syntax.string_of_term @{context}) *}
 
-ML {* f 1 |> (Option.map o map) (Sign.string_of_term @{theory}) *}
-ML {* f 2 |> (Option.map o map) (Sign.string_of_term @{theory}) *}
-ML {* f 3 |> (Option.map o map) (Sign.string_of_term @{theory}) *}
-ML {* f 4 |> (Option.map o map) (Sign.string_of_term @{theory}) *}
-ML {* f 5 |> (Option.map o map) (Sign.string_of_term @{theory}) *}
-ML {* f 6 |> (Option.map o map) (Sign.string_of_term @{theory}) *}
-ML {* f 10 |> (Option.map o map) (Sign.string_of_term @{theory}) *}
-ML {* f 10 |> (Option.map o map) (Sign.string_of_term @{theory}) *}
+ML {* f 1 |> (Option.map o map) (Syntax.string_of_term @{context}) *}
+ML {* f 2 |> (Option.map o map) (Syntax.string_of_term @{context}) *}
+ML {* f 3 |> (Option.map o map) (Syntax.string_of_term @{context}) *}
+ML {* f 4 |> (Option.map o map) (Syntax.string_of_term @{context}) *}
+ML {* f 5 |> (Option.map o map) (Syntax.string_of_term @{context}) *}
+ML {* f 6 |> (Option.map o map) (Syntax.string_of_term @{context}) *}
+ML {* f 10 |> (Option.map o map) (Syntax.string_of_term @{context}) *}
+ML {* f 10 |> (Option.map o map) (Syntax.string_of_term @{context}) *}
 
 ML {* val f = Quickcheck.compile_generator_expr @{theory}
   @{term "\<lambda>(s \<Colon> string). s \<noteq> rev s"} [@{typ string}] *}
 
-ML {* f 4 |> (Option.map o map) (Sign.string_of_term @{theory}) *}
-ML {* f 4 |> (Option.map o map) (Sign.string_of_term @{theory}) *}
-ML {* f 4 |> (Option.map o map) (Sign.string_of_term @{theory}) *}
-ML {* f 4 |> (Option.map o map) (Sign.string_of_term @{theory}) *}
-ML {* f 10 |> (Option.map o map) (Sign.string_of_term @{theory}) *}
-ML {* f 10 |> (Option.map o map) (Sign.string_of_term @{theory}) *}
-ML {* f 10 |> (Option.map o map) (Sign.string_of_term @{theory}) *}
-ML {* f 10 |> (Option.map o map) (Sign.string_of_term @{theory}) *}
-ML {* f 10 |> (Option.map o map) (Sign.string_of_term @{theory}) *}
-ML {* f 8 |> (Option.map o map) (Sign.string_of_term @{theory}) *}
-ML {* f 8 |> (Option.map o map) (Sign.string_of_term @{theory}) *}
+ML {* f 4 |> (Option.map o map) (Syntax.string_of_term @{context}) *}
+ML {* f 4 |> (Option.map o map) (Syntax.string_of_term @{context}) *}
+ML {* f 4 |> (Option.map o map) (Syntax.string_of_term @{context}) *}
+ML {* f 4 |> (Option.map o map) (Syntax.string_of_term @{context}) *}
+ML {* f 10 |> (Option.map o map) (Syntax.string_of_term @{context}) *}
+ML {* f 10 |> (Option.map o map) (Syntax.string_of_term @{context}) *}
+ML {* f 10 |> (Option.map o map) (Syntax.string_of_term @{context}) *}
+ML {* f 10 |> (Option.map o map) (Syntax.string_of_term @{context}) *}
+ML {* f 10 |> (Option.map o map) (Syntax.string_of_term @{context}) *}
+ML {* f 8 |> (Option.map o map) (Syntax.string_of_term @{context}) *}
+ML {* f 8 |> (Option.map o map) (Syntax.string_of_term @{context}) *}
 
 ML {* val f = Quickcheck.compile_generator_expr @{theory}
   @{term "\<lambda>f k. int (f k) = k"} [@{typ "int \<Rightarrow> nat"}, @{typ int}] *}
 
-ML {* f 20 |> (Option.map o map) (Sign.string_of_term @{theory}) *}
-ML {* f 20 |> (Option.map o map) (Sign.string_of_term @{theory}) *}
-ML {* f 20 |> (Option.map o map) (Sign.string_of_term @{theory}) *}
-ML {* f 20 |> (Option.map o map) (Sign.string_of_term @{theory}) *}
-ML {* f 20 |> (Option.map o map) (Sign.string_of_term @{theory}) *}
-ML {* f 20 |> (Option.map o map) (Sign.string_of_term @{theory}) *}
+ML {* f 20 |> (Option.map o map) (Syntax.string_of_term @{context}) *}
+ML {* f 20 |> (Option.map o map) (Syntax.string_of_term @{context}) *}
+ML {* f 20 |> (Option.map o map) (Syntax.string_of_term @{context}) *}
+ML {* f 20 |> (Option.map o map) (Syntax.string_of_term @{context}) *}
+ML {* f 20 |> (Option.map o map) (Syntax.string_of_term @{context}) *}
+ML {* f 20 |> (Option.map o map) (Syntax.string_of_term @{context}) *}
 
 end